[fsloth]

I presume when you exclaim "type-theoretic monstrosities" I presumes you have some specific language in mind?

For example, in F# types maintain program correctness but get out of the way. They're not about obstinate bureaucracy but a way for the compiler to remind me "dude, this is not doing what you earlier specified it should do" and then I observe that yes, I've forgotten some corner case, do a small modification to the type definition and the whole damn thing works.

If types are getting in the way then the language is not very good (by my definition C++ is not very good and I mostly earn my living writing it).