alt Hacker NewsYou also have the problem of potentially having to re-verify everything by hand for every little change. Maybe fine for the kinds of projects Dijkstra was working on, but less practical in a business setting.
Tools like QuickCheck and Hypothesis are an interesting middle ground, though. I strongly prefer them over standard-issue unit testing for verifying algorithm implementations.
Hundred percent. All about trade-offs.
Although proof techniques such as proof repair have come a long way, it’s still impractical for a lot of scenarios.
TLA+ is great for systems design and such. Quick check style tests are awesome and a very low bar to clear from unit tests.