3 ms·
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 fut
by disown 6y ago
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.
- xmprt 6y agoProofs 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.
- MaxBarraclough 6y agoYou seem to be dismissing formal methods, but they've been used successfully in various domains.
- chas 6y agoThe control systems for airplanes often have a significant number of mathematical proofs.
- nimish 6y agoSure because the alternative is death Me shit posting is not a life or death situation so a bug here or there is fine
- thereisnospork 6y agoThe bolts don't, and yet they don't (usually) fail.
- feteru 6y agoWhat do you mean? They're designed and tested according to calculations done by mathematically proven methods.
- compiler-guy 6y agoBut 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.
- 6nf 6y agoEvery single bolt on a plane is tracked from the steel foundry to retirement with serial numbers and testing and certification and everything.
- war1025 6y agoMy 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.
- 6nf 6y agoDonald Knuth quote: Beware of bugs in the above code; I have only proved it correct, not tried it.
- ahelwer 6y agoFormal 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.
- roenxi 6y agoIf 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.
- IncRnd 6y agoA proof is only performed under certain assumptions and is far from a logical certainty for all time.
- jacquesm 6y agoLate 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.