Thus quoth David McClain at 22:47 on Tue, Apr 18 2017:
Excellent point you make about type checking versus provably correct code. I probably allowed myself to be lulled by a false equivalence many times in the past, confusing one for the other under pressure to get something working. But then, how many programmers actually produce provably correct code? I can see that happening very easily in the small. But for overall large programs?
According to my knowledge, as well as to the unverified remark on Wikipedia [0], not so many people prove their software correct. That's probably because current formal verification methods require a lot of effort and have trouble supporting somewhat variable end-user requirements within reasonable time bounds. -- Sergiu [0] https://en.wikipedia.org/wiki/Formal_verification#Industry_use