This is precisely what an effect system is, and what the languages that I mentioned do. So it seems that you agree with the the church of lambda on this p

This is precisely what an effect system is, and what the languages that I mentioned do. So it seems that you agree with the the church of lambda on this point? No, Eff starts with a pure lambda calculus and adds effects on top. I've explained several times that the assumption that you need to do full on verification from the start with a CH style system is incorrect. You can write your prototype without any verification and add lemmas and theorems about it when the spec stabilizes. As I said, I don't really see that. There is research going on, like the aforementioned Trelly that seeks to build such systems, but they are not there yet. Well yes, you also need "well typed programs don't go wrong" of course, which dependent type systems do have. Well typed programs do go wrong! Here is a well-typed Ocaml program: List.hd [];; When I run it, an exception is thrown. The point is: what counts as "not going wrong" is a fairly arbitrary definition. And for the trivial typing system I can define programs that go wrong as the empty set. I don't think decidability of type checking is desirable, by the way. What you really want is a system that checks statically as much as possible, but can check dynamically that which it can't verify statically. Rather than two possibilities "correct" vs "incorrect" you want three: "definitely correct", "definitely incorrect" and "can't determine statically, so let's check dynamically". In the last case conventional systems just reject the program as incorrect, but I think that is not as helpful. I don't think this will be useful, because than every typo will turn into a dynamic check, and you end up with a dynamically typed language for all practical purposes. I think More open than a program logic system that does the same? Yes, vastly more open. Those problems are essentially solved for program logics. I don't think the approaches are that different in this regard. With state/concurrency/etc you work with a description of the computation Yes, you can work by encoding, but then you pay the "encoding tax" in verification. The dynamic checks are for when type checking fails, not type inference. The type inference will always infer the type if the term is typeable. That's not how I understand the Sage paper [1], which says: "Our implementation performs bidirectional type checking (Pierce and Turner 1998), allowing many types to be inferred locally, but does not yet perform full type inference (a much more technically challenging problem)." That paper itself says so in the first sentence? But the paper also presents a complete inference algorithm for GADTs. The point is: it depends on exactly what you mean by GADTs. I don't know what Ocaml does here. I stopped using Ocaml just before GADTs were added. [1] https://sage.soe.ucsc.edu/sage-tr.pdf https://sage.soe.ucsc.edu/sage-tr.pdf