4 ms·
You're not verifying a language, you're verifying a program (or some part of one). Sure- that part in this instance may be implementing a language standard lib
by emn13 9y ago
You're not verifying a language, you're verifying a program (or some part of one). Sure- that part in this instance may be implementing a language standard library, but who cares? That program also has tests, docs, types and all the other things people use to convince themselves of correctness.
It really is like unit testing. There too you could make the argument that in some cases untestable code might be worth it if the alternative is an api that's hard to use. And there too an api may well be used many orders of magnitudes more frequently than it is changed. I think you have to decide that on a case by case basis (at least, I can't think of any convincing general argument there).