Curry-Howard Is a Scam

Program in CH has its own definition, which is typically not like “useful” programs that people write in real world. So it doesn’t really promise what it might seem to offer on the surface.

On the other hand, formal verification of programs is indeed not as useful as advertised. But it is simply because most of the time people don’t really care about edge cases. Many programs don’t even have decent test suite, not to say proof!

Title change to "is overrated"