[yorwba]

> Types do not usually capture semantics - unless we are talking about something a lot more powerful than what I'm used to seeing in real programming languages.

You are right, I should have specified that the correctness proof only applies to properties actually given in the type system. So for a high-stakes financial application, your types should be strong enough to capture at least elementary arithmetic. This is definitely not something you'd see in a mainstream programming language.

> It's not the types that tell me what arbitrary properties my code should have!

When you give a variable in a program a type, you assert a property for all values that variable will ever take. The converse is also true: for any property you want to express, there is a type system that can encode it. This is called the Curry-Howard correspondence.

Unfortunately, most interesting properties one might want to formalize require either an undecidable type system, or you have to write a bunch of proof code just to convince the type checker that the rest of the code conserves the properties it should. That isn't too different if you'd be doing formal verification for all your code anyway, but it gets annoying when it is enforced everywhere, even when you'd deem it unnecessary otherwise. In that, it is similar to a policy of "unit tests everywhere", which probably catches some bugs, but also leads to lots of boilerplate stating the obvious.