2 ms·
>I find it much easier to formally verify things correct than to test that they're correct. This rise in me the famous joke by Knuth: Beware of bugs in the abo
by psychoslave 5y ago
>I find it much easier to formally verify things correct than to test that they're correct.
This rise in me the famous joke by Knuth: Beware of bugs in the above code; I have only proved it correct, not tried it.
I wonder which tools he uses to prove correctness, and on which language. I know about Frama-C, Coq, and things like that. But I never had the opportunity to use them out of university. On the same topic, in a recent ACM publication, Ian Joyner compare Frama-C with a lipstick on a Pig.
https://cacm.acm.org/magazines/2021/12/256941-common-ails/fulltext https://cacm.acm.org/magazines/2021/12/256941-common-ails/fu...
- kqr 5y agoIn that case I think Knuth referenced proving it by hand, e.g. with Hoare triples. You could argue that hand proof is useless, but by forcing yourself to go through it in tiny steps you can actually sort out a lot of oversights.
- edwcross 5y agoC is a pig of a language, so tools that show just how horrible it is, how many bugs are unwittingly written, and how hard it is to make its code safe, could also help pushing people towards better languages. These tools are more like putting on X-ray glasses and seeing how your fast-food nuggets are made. You will still eat them if you have to, or if you're in a hurry, but you'll be more inclined to take the time to learn cooking, so you can eat healthier food later.