2 ms·

Not to me. I've found unit tests to be indispensable in establishing and maintaining code correctness -- and my unit tests have always been written in a PL, too

• lomnakkus 11y ago
  There are two cruical properties you want, I think: A) It must be possible to automatically and completely mechanically ensure that implementation & proof don't get out of sync. Having a formal proof for an algorithm which isn't the algorithm that you've actually ended up implementing doesn't really help you one whit :). This is relatively simple for unit tests and property-based tests like QuickCheck: Just observe that the number of tests run actually increases over time and never decreases unexpectedly. (Actually, it seems to be rather rare to have support from Continuous Integration tools for tracking the latter.) B) There must be (in some sense) at least some non-trivial difference between the implementation & "proof". (At the absurd extreme: bisimulation doesn't really work as proof of anything if the implementations are one and the same.) For example, in Idris the implementation is basically just code while the proof is the accomanying types -- which ensures that they're not basically just saying the (trivially) same thing, even though the types greatly constrain what the implementation can do. I think that the allure of "practical" dependent types (e.g. Idris) may be that such languages trivially obey both properties. Of course you still end up with a "trusted computing base" which is non-trivial in such cases.