I said "Note I mean proven correct, proven to do exactly as specified, not just proven to lack certain classes of bugs.". Model checkers don't prove functional

I said "Note I mean proven correct, proven to do exactly as specified, not just proven to lack certain classes of bugs.". Model checkers don't prove functional correctness, they just prove the absence of certain kinds of bugs. Sure, if you don't care about correctness model checkers are great, but if you do care about proving a program does exactly as specified then you'll have a much easier time with a functional language.