The problem with proof is that it’s a bit hard sometimes to convey the value. The point is not to find bugs, but to prove that there are none (of a certain class; under certain assumptions; etc). But it’s a hard story to sell, so often the marketing is around “look at this bug we found”.
replyYes. Most people don’t actually understand what a program proof is - the answer is usually ‘I have very good tests’.
replyNow, go write the code for an artificial heart , and sleep at night thanks to strong testing !
I would be much more interested in "here is a provably memory safe version of openssl with all its memory safety bugs fixed"
reply