While I also agree that static typing is the easiest, statically decidable way to significantly increase program correctness, I’m not sure we can do significant

While I also agree that static typing is the easiest, statically decidable way to significantly increase program correctness, I’m not sure we can do significantly better with it then we currently do. Most interesting properties are not expressible even with dependent types, and those are very hard to prove, making their advantages non-no-brainers. What I’m trying to say is that we should be open about another concept, for example contract-based programs (clojure’s spec for example), because they might have better properties.