That might ironically go better starting from a Lisp-like dynamic language. "Just add types". Because the static typing side is hard, advancing one paper and

That might ironically go better starting from a Lisp-like dynamic language. "Just add types". Because the static typing side is hard, advancing one paper and thesis at a time. The poorly-funded multi-decade creeping installment plan of progress. Even with category theory, the overwhelming emphasis is on using it for proof rather than for its expressiveness. A fun example... from a very collegial course in pre-Covid January, sniff... Categories work over PreSets - no predicate of member equality required. But say I claim to be handing you a PreSet. You can't verify that claim. Your ability to prove anything is very limited. Sad for mathematicians. But fine as API. But that's not where attention is.