4 ms·
Formal verification is very cool and definitely has its uses (https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf https://www.sigops.org/s/co
by eterevsky 3y ago
Formal verification is very cool and definitely has its uses (https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf https://www.sigops.org/s/conferences/sosp/2009/papers/klein-...). From what I heard at least some chip manufacturers do formal verification of their chip designs.
But I don't think it scales to general-purpose programming. Most of the easy-to-verify conditions could (and should) be checked by asserts and unit tests. But there's a whole layer of complexity on top of that and in my experience it accounts for the bigger share of bugs.
- tempodox 3y agoThat's like saying that motor-driven vehicles are not for common use an that your vehicle could and should be driven by a horse.
- Linell 3y agoHow?
- RGBCube 3y agoIf it was easier to use, manouver and maintain a horse, your claim would be true.
- eterevsky 3y agoSorry I wasn't clear. I didn't mean to imply that languages with formal verification are inherently worse than those without it. To the contrary, if a language would have formal verification in addition to all the features and an ecosystem of a modern language, I would gladly use it. My point is that for most use cases formal verification by itself is less important than all the other stuff.
- tempodox 3y agoI understand, and I concur.