[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Adam Chlipala]

I'm curious about the pragmatic effects of the different adequacy proof 
techniques that these different tools allow.  If every technique has 
some amount of informality, then the question seems to be what effect 
the differences in informality have on real "logic engineering."

Does anyone have any cautionary tales of adequacy problems with machine 
formalizations, perhaps accompanied with explanations of how using a 
different tool would have avoided the problem?