Welcome to European Tribune. It's gone a bit quiet around here these days, but it's still going.
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 ]

Others have rated this comment as follows:


Top Diaries

Latest Data Omicron Variant

by Oui - Nov 30

Sweden almost has a new PM

by fjallstrom - Nov 26

Ten Days That Redefined PM Johnson

by Oui - Nov 14

Salman's Saudi Tiger Squad

by Oui - Nov 7

Occasional Series