Hacker News Reader

Comment by disown | Hacker News Reader

Because reliable and proof are not the same concepts and one is not needed for the other. Proof is logical certainty for all time ( in the past, present and future ). Reliability is not.

Reliability doesn't require mathematical proof - this goes for airplanes to your kitchen faucet to software. Software became more and more reliable through testing, errors, fixes/patches, etc. Also, many times good enough is good enough. We don't need the perfect for most situations.

Also, it's a subjective call too. For some software is an unreliable mess and we need to throw everything out and rebuild it from scratch. Search for haskell, rust, etc threads. The neverending arguments against side-effects, mutation, pointers, etc. For most, they are good enough and get the job done.

View on HN

The control systems for airplanes often have a significant number of mathematical proofs.

Sure because the alternative is death

Me shit posting is not a life or death situation so a bug here or there is fine

The bolts don't, and yet they don't (usually) fail.

What do you mean? They're designed and tested according to calculations done by mathematically proven methods.

But that isn't formal verification via mathematical proof. And this is the crux of the flaw with the paper. There are lots of ways to reliability. Mathematical proof is just one.

Every single bolt on a plane is tracked from the steel foundry to retirement with serial numbers and testing and certification and everything.

My father-in-law works on control systems for airplanes and I get the impression that it's based much more on testing in flight simulators than on any amount of proofs.

The level he works at might be higher level though. It sounds like control systems for airplanes are fairly modular.

Donald Knuth quote: Beware of bugs in the above code; I have only proved it correct, not tried it.

Formal methods aren't as widespread in safety critical industries as you might hope or believe. Model-based testing is still considered cutting edge, never mind formal verification.

Formal verification is only as good as your model, anyway. Problem comes from outside your model? Formal verification won't save you.

If it is possible to use proof that is lovely; but it isn't necessary. Things have been engineered to very high levels of reliability with only the most tangential reliance on proofs.

Software is highly unusual in that proofs can even be deployed. Most highly safe processes can't even use proofs. How do you prove that a dam won't fail? It is impossible.

Proofs are only valid as long as the requirements don't change and assumptions are still valid. Two things that any first year CS student could tell you are absurd to even imagine.

You seem to be dismissing formal methods, but they've been used successfully in various domains.

Late to the party, sorry for the delayed answer. That's a very important observation you are making there. I think another one to complement it is that reliability does not make any assumptions about underlying systems performing as advertised, including the hardware. Many (all?) formal verification methods do make that assumption.

A proof is only performed under certain assumptions and is far from a logical certainty for all time.

Reply on news.ycombinator.com