[ltr_]

I agree with your sentiment and resonate with some of my opinions on languages (been reading about TT and abstract math in general for a while as a hobby)

my opinions so far (subject to change as i read more):

dynamic typing = just one type [0]. yes, good to test ideas quick, to develop quick gigs that i don't care about and tiny snippets/scripts, i use js for that.

gradual typing = guaranteed mess evolving large code bases, I guess the gradual typing thing in practice never happen and when it happens your IDE becomes red and your compiler errors explode, i don't recall where i read about that but it made sense to me, i used groovy to take advantage of the optional typing but i was the only dev in that project.

sound type system + parametric polymorphism = the best thing around, although i prefer to have explicit type annotations.

no formal math object behind a language = the language does not exist, just , absurd rules ,idioms and syntactic mess that you have to remember and tied to specific monkey patched implementations to compensate incoherent foundations, sadly unavoidable, as most, if not all popular languages do not exist,.

Yes, I've been reading Harper a lot.

[0] https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...

edit: formatting