>What he want's are languages that explore making them ergonomic at the language level.
This is exactly what dependently typed languages like coq and idris are attempting to do. What he wants ALREADY exists and these things are trying to fulfill EXACTLY his intent. I am not attempting to talk about some obscure isomorphism.
You also cannot build all 6 things in any number of languages unless you are using those languages to build new languages. These checks exist at the type level, not at runtime, but pre-compile time.
I think what you are missing is that the author of the article does not consider the affordances of those languages as sufficient exploration of the space. Just because they can express these things and are meant to fulfill his intent doesn't mean they succeed in the ways he wants.
This is exactly what dependently typed languages like coq and idris are attempting to do. What he wants ALREADY exists and these things are trying to fulfill EXACTLY his intent. I am not attempting to talk about some obscure isomorphism.
You also cannot build all 6 things in any number of languages unless you are using those languages to build new languages. These checks exist at the type level, not at runtime, but pre-compile time.