[brianberns]

Actually, one of the benefits of strong typing (without side effects) is that the correct implementation is sometimes the only one that compiles.

For example, if you know that a function takes a generic list and returns an integer, then the list’s length is pretty much the only non-trivial computation it can perform.

[ericelliott]

I've seen this happen for a handful of functions, but implementation correctness proofs for general applications are far beyond the expressive capabilities of TypeScript.