Comment by lou1306

> people who aren't able to write correct code are somehow able to write correct mathematical specifications

This describes about one or two thirds of the Theoretical CS academic community (conservative estimate) /s

> This is quite an extraordinary claim given that the mathematical specification is an order of magnitude longer and more complex than the code itself

I find this hard to believe. The mathematical specification for "array a is sorted" is "forall n in Nat: 0 < n < len(a) -> a[n] >= a[n+1]". The average sorting algorithm is usually a tad longer than this.

> the mathematical spec would get completely invalidated every week or so each time you did an update

Well of course nobody serious advocates for formalizing/verifying code that is subject to that much churn (be it internal or external).