> And the correctness is limited only to certain properties of the program, that a given type system supports. In case there are readers not familiar with the

> And the correctness is limited only to certain properties of the program, that a given type system supports. In case there are readers not familiar with the current state of things, you can pick solid languages today whose type systems support a LOT. It is completely fair (and good) to point out that this isn't a panacea, but it can significantly help.