> Type systems like those in Java and C# give you very little formal verification [...] What Java-like type systems give you is confidence in refactoring, which is not nothing, but it is not formal verification.
You might be surprised to hear that you can prove a large class of programs correct using plain ol' Java types [1].
You might be surprised to hear that you can prove a large class of programs correct using plain ol' Java types [1].
[1] http://lambda-the-ultimate.org/node/5387