The difference is in what a developer can express. As has often been noted: you can write FORTRAN in any language. But that doesn't mean I will opt for Fortran

The difference is in what a developer can express. As has often been noted: you can write FORTRAN in any language. But that doesn't mean I will opt for Fortran (except perhaps for some specific numeric computing cases! Then I might!) when other tools allow me to capture more invariants in my program. The fact that the compiler doesn't make me is orthogonal to the point I was getting at in this article. It allows me to capture constraints and invariants that matter to me, and it enforces certain constraints and invariants on all developers. That combo can be—and in my experience working a lot in C and JS as well as in richly typed modern languages like TS, Rust, Elm, etc.—very, very powerful and rewarding. (Also: TS gets surprisingly far on dynamic runtime inspection. While I'd love to see the ideas in Idris become far more mainstream, in the meantime, the stuff TS is doing with type narrowing, mapped types, conditional types, and so on is nothing short of astounding. You can do some pretty wild stuff that isn't quite dependent types but gets awfully close. But caveat emptor: compile times may get you.)