3 ms·
The problem is that these formal proof systems are often marketed as tools to write "bug free code". You will see statements along the lines of "this code is pr
by david-gpu 9y ago
The problem is that these formal proof systems are often marketed as tools to write "bug free code". You will see statements along the lines of "this code is proven to be bug-free", etc. They over-sell and under-deliver.
When you also consider that performing these proofs takes a very significant amount of time, you end up with something with very limited applicability for the vast majority of software development scenarios.
That's all I'm saying. Please don't argue against a strawman.
- icebraining 9y agoCan you provide an example of a system being marketed as a tool to write "bug free code"? I saw nothing of the sort in the sites of Coq, TLA+ or Isabelle. Are you sure you're not the one arguing against a strawman?
- deleted 9y ago[deleted]
- david-gpu 9y agoIn these comments there are several examples of folks selling an algorithm as "proven" and later turning out to be buggy.
- icebraining 9y agoRight, because they are proven. It's your assumption that proven == bug-free that is incorrect.
- dtornabene 9y agoYou mean like, say, seL4? Pretty sure that kernel is seeing some very real "applicability".