Comment by mpweiher

"Beware of bugs in the above code; I have only proved it correct, not tried it."

   Donald Knuth

--

> doesn't give big payoffs.

I think that's the key here. The idea that proving things correct means they are flawless is...fancyful. And the expense is very high.