[ique]

What you're saying is just "trusting any system is insane", which sure, it might be (depending on the criticalness of said system).

But that's not very insightful or informative, how does that drive any sort of decision-making or improvement process?

Do you have any suggestion on how to improve the correctness of systems that work better than formal verification?

[oldgradstudent]

Formal verification techniques can be very useful, especially for finding deep, often insanely complex bugs.

The process of developing the proof can produce a lot of insight about the system and expose hidden assumptions that were never considered while designing the system.

It is the final proof itself which is the problem. It does not contribute anything except for terminating the debugging process.

Because the specification can be just complex as the system, the proof can only provide a false sense of security. A correctness theatre.

[tom_mellior]

> It is the final proof itself which is the problem. It does not contribute anything except for terminating the debugging process.

That's true in a certain restricted sense, if you see the verified program as a thing set in stone and never touched again. But verified software is maintained, changed and extended just like other software. Whenever you change a program and your proofs still work, that tells you something. If the proofs break, that also tells you something. If all you need to change are some small lemmas but the overall end-to-end proof goes through, you know exactly what interactions with other parts of the system were affected by your change.

[Silhouette]

Because the specification can be just complex as the system

That's true in principle, but in practice I don't think it's going to hold in most cases. A good specification necessarily captures the essential complexity of the system, but it's a lucky developer whose implementation doesn't introduce considerable accidental complexity as well. Ensuring that this accidental complexity doesn't break anything could have great value, depending on the nature of the system and how damaging a failure could be.

[zzzcpan]

This is what many people are missing in their understanding of formal verification. Things that reduce bugs are not proofs, but a different thought process that sort of double checks everything from a different perspective.

[seanwilson]

> Because the specification can be just complex as the system

Can you give an example of this? I don't find this true in general at all e.g. writing the specification of a sorting algorithm is much easier than implementing most practical sorting algorithms.

> the proof can only provide a false sense of security. A correctness theatre.

You could use this argument to say that unit tests, type systems, code review etc. are correctness theatre. All these things prevent mistakes.

[mafribe]

> Can you give an example of this?

It's pretty clear that a fully formal specification of a program must be (roughly) as complex as the program itself, for otherwise you could construct an infinitely descending chain of ever simpler specifications which leads to a contradiction.

The reason that you found the specification of a sorting algorithm simpler than the sorting algorithm is that you probably have not fully specified the algorithm. Consider the sorting algorithm in C's standard library, which allows the user to specify a comparison function. Now imagine you'd pass something like the following comparison function:

   def compare (x, y):
      printf ( "I'm comparing %i with %i\n", x, y )
      if ( x < y ) return 1
      if ( x == y ) return 0
      else return -1

It almost completely exposes the inner workings of sorting. Hence a full spec needs to account for this.

[seanwilson]

> It's pretty clear that a fully formal specification of a program must be (roughly) as complex as the program itself, for otherwise you could construct an infinitely descending chain of ever simpler specifications which leads to a contradiction.

That's like saying a theorem statement must be roughly as complex as the proof.

Also consider that it's much harder to reason (and prove) that heavily optimised versions of algorithms are correct compared to naive implementations. For example, a proof of correctness for heapsort is more involving than one for insertion sort.

[profquail]

Check out the article(s) about Amazon’s use of TLA+ for a good, industrial example of formal methods:

http://lamport.azurewebsites.net/tla/amazon.html

[abritinthebay]

Trusting any sufficiently complex system to be correct is insane. It’s virtually impossible to do and be confident at all levels your proof is correct once you move past much more than trivial systems.

This is why modern software testing takes a more... I guess you could call it Bayesian... approach.

QA, unit testing, integration testing, etc - these are all ways of reducing probabilities of incorrectness. Never formally prove it of course, but make your confidence higher with each.

So suggestions? Proper testing and QA.

[lmm]

> QA, unit testing, integration testing, etc - these are all ways of reducing probabilities of incorrectness. Never formally prove it of course, but make your confidence higher with each.

And formal proofs don't make your confidence higher? IME they're the most efficient tool in the toolbox if you need to get to really low defect rates. (Of course, the sad economic reality is that for most consumer software even a 5% defect rate is perfectly acceptable).

[zzzcpan]

It's not that simple. Defects don't necessarily have to cause problems, depending on how you design your software (think OTP-style architecture). And avoiding problems is in fact what you always need, not low defect rates. It's just so happens that sometimes you can only achieve decent reliability by pursuing very low defect rates. But for a lot of software it cannot economically beat other approaches.

[abritinthebay]

Given a formal proof of a complex system that doesn’t contain any assumptions or mis-modeling is - practically speaking - unachievable...

... then in comparison the time is better spent on something that will produce demonstratable results, even if imperfectly applied.

And that is QA & testing.

[lmm]

> the time is better spent on something that will produce demonstratable results, even if imperfectly applied.

How is formal proof not such a thing?

[edanm]

QA testing on various levels, and real-world usage without incident?

This is what most software does and it seems to work fine in the real world, in most cases at least.

[hateduser2]

>it seems to work fine in the real world

I thought the whole premise of this conversation was that this is a total fabrication?

[abritinthebay]

I don’t believe so - I think it was it isn’t formally showing it is correct. Which is true.