Hacker News Reader

Static type checking is abstract interpretation. If you program in Java you are using formal methods.

So we do use formal methods! Problem solved.

The proofs you produce are probably weaker than those the author wants