3 ms·
The control systems for airplanes often have a significant number of mathematical proofs.
by chas 6y ago
The 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.