We don't write / maintain code we understand, we at best write / maintain code we think we understand. Often bugs come and then we realize we did not understand what we or others wrote. While I agree that provable code is too hard, and that we should put effort in making code clear, and document intentions this is only a small part of writing reliable and safety critical code. What we need to look at is fault tolerance in our tooling, (eg erlang) and more effective testing (eg QuickCheck).
No one is capable of writing tools that will prove that their code works and is well engineered because no one knows how to write code that works and is will engineered simply because it's that difficult of a subject. Whoop-de-doo!
Who on earth would submit a patch with code that doesn't compile? That's careless at best! (35:36)
We don't write / maintain code we understand, we at best write / maintain code we think we understand. Often bugs come and then we realize we did not understand what we or others wrote.
While I agree that provable code is too hard, and that we should put effort in making code clear, and document intentions this is only a small part of writing reliable and safety critical code.
What we need to look at is fault tolerance in our tooling, (eg erlang) and more effective testing (eg QuickCheck).
+Owen Synge Maybe. For certain things (eg distributed systems) I increasingly think nothing meaningful can be created without proofs.
40 minutes wasted. Thanks.
No one is capable of writing tools that will prove that their code works and is well engineered because no one knows how to write code that works and is will engineered simply because it's that difficult of a subject.
Whoop-de-doo!