I’m on my phone so I can’t really give this the response that it’s owed, but most of what I want to say is that I don’t think we disagree as much as you think. My mention of languages being the wrong approach to general programming is a key aspect of my position. You’re right that DSL’s are usually not a great idea, but that seems like more of an issue with the “syntax-chasing”. The affordances that a syntax forces upon everyone are why it takes a decade to add generics to Go and why macros are even used to begin with. As we see from the various notations used for equivalent math, we probably we be better off encoding the structure as a flexible semantics graph and then “projecting the syntax” however the programmer wants. Keep in mind that what I write is about possibilities more than what you would be forced to do every project. You wouldn’t expect everyone to import random type systems more than you would expect everyone of write and import their own random crypto system libraries.
Some of the most popular languages out there have absolutely zero static checks. Would it be so bad to write a Turing complete static check function? Why do we care so much about decidability that we can’t even consider it in useful exceptions? Also, do you think macros a la lisp would be so bad if they had more powerful type systems backing them up and more flexible editors to understand them?
> Would it be so bad to write a Turing complete static check function?
I think most type systems are, in fact, Turing complete (there's a fun proof somewhere that TypeScript is, for example). And most typed languages (Go, C++, Java, TypeScript) have pretty mature static type-checkers, unless I'm misunderstanding your ask.