Welcome to European Tribune. It's gone a bit quiet around here these days, but it's still going.
Display:
See Formal verification. I remember some of this from an introductory programming course in my math degree 20 years ago. It was fascinating but evidently the amount of resources needed for algorithm verification of anything but the simplest algorithms was prohibitive. In addition, we only saw how this applied to simple procedural languages. Real, modern computer systems are full of event-driven programs, hardware interrupts, declarative languages, and what-not. Algorithm verification is probably only useful as a debugging technique, not for a-priori certification of real life programs.

Finance is the brain [tumour] of the economy
by Migeru (migeru at eurotrib dot com) on Mon Jun 10th, 2013 at 02:48:50 PM EST
[ Parent ]
Basically you can prove reliability if there's a finite number of program states and execution paths, you can specify the transitions through/between them, and then prove you're not in some kind of NP tar pit.

Which is fine as far as it goes. But - as you say - most software is event driven, and doesn't run like a sausage factory where stuff goes in, you wait a while as things happen, and stuff comes out.

So in practice you can't even completely specify the inputs, never mind define states/paths/transitions.

And then there are horrible things like natural language interfaces, where the semantics are inherently fuzzy and there is often no unambiguous meaning at all.

In fact I think there's going to be an eventual singularity in software development, where formal systems become smart enough to define improved formal systems. We'll probably get software proving that software sort-of works by the end of the decade, and certainly by the end of the 2020s.

Once humans no longer have to write code by hand, development will speed up a lot and become much tidier and more reliable.

by ThatBritGuy (thatbritguy (at) googlemail.com) on Mon Jun 10th, 2013 at 03:16:37 PM EST
[ Parent ]
Formal Systems will never be able to verify formal systems until we can make an end-run around Gödel's incompleteness theorems.  Which, at the moment, is a lot like saying, "We can achieve FTL when we make an end-run around the Theory of Relativity."

She believed in nothing; only her skepticism kept her from being an atheist. -- Jean-Paul Sartre
by ATinNM on Mon Jun 10th, 2013 at 04:11:52 PM EST
[ Parent ]
That there are undecidable questions of arithmetic doesn't mean that every algorithm verification is undecidable.

Finance is the brain [tumour] of the economy
by Migeru (migeru at eurotrib dot com) on Mon Jun 10th, 2013 at 04:23:49 PM EST
[ Parent ]
I agree some can be.  

At a former job I verified a program's algorithm would accomplish the required task and then halt.  I also found it would halt after ~600 years.  Thus it wasn't Formally NP ...

& whoop-de-do

Computer Engineering is engineering.  As such it is different than the tools: Logic, Maths, etc., it uses.  Axiomatic Deductive Logic is a nice tool.  In all too many cases using only ADL is a sure route to, "How the %$^@#$! did we get into THIS mess?"

She believed in nothing; only her skepticism kept her from being an atheist. -- Jean-Paul Sartre

by ATinNM on Wed Jun 12th, 2013 at 01:36:44 PM EST
[ Parent ]
Axiomatic Deductive Logic

No, no it's not. Just no. Bleurgh.

by Colman (colman at eurotrib.com) on Wed Jun 12th, 2013 at 01:38:55 PM EST
[ Parent ]
We have to be gentle with Migeru.  His mind has been warped by Physics.

She believed in nothing; only her skepticism kept her from being an atheist. -- Jean-Paul Sartre
by ATinNM on Wed Jun 12th, 2013 at 03:42:41 PM EST
[ Parent ]
was formulated explicitly for number theory. There are two parts (from 40 year old memory):

  1. Any theorem that is capable of proving as true only theorems that are true is not capable of proving as true all theorems known to be true.

  2. Any theorem that is capable of proving as true all theorems known to be true will also prove as true theorems known not to be true.

Of the types of theorems described the first category seems the more useful. Even though it was first developed for number theory it has not prevented us from doing accurate calculations. (Which was always my problem to begin with  :-)

"It is not necessary to have hope in order to persevere."
by ARGeezer (ARGeezer a in a circle eurotrib daught com) on Tue Jun 11th, 2013 at 10:55:10 AM EST
[ Parent ]
In fact I think there's going to be an eventual singularity in software development, where formal systems become smart enough to define improved formal systems. We'll probably get software proving that software sort-of works by the end of the decade, and certainly by the end of the 2020s.

I'd say about fifty years.
by Colman (colman at eurotrib.com) on Tue Jun 11th, 2013 at 05:25:34 AM EST
[ Parent ]
Model checking is already useful for finding subtle bugs in reactive controller programs. But those methods are only used on safety-critical projects. Avionics, nuclear reactor controller etc.

However, the general verification/synthesis problem cannot be automatically solved (there is a proof).

Schengen is toast!

by epochepoque on Thu Jun 13th, 2013 at 07:11:23 PM EST
[ Parent ]

Display:

Top Diaries

Occasional Series