@pnathan So what formalism (I'll use that word instead of 'language', to reinforce that I do NOT mean 'compiler and typesystem' but something simpler and deeper) can I use to compare and contrast the type and function and data semantics of Rust, Go, Swift, D, ObjectiveC, Java, Elm?
What primitives must that formalism have? What's the smallest, simplest possible core?
So far I guess Inductive Calculus of Constructions is the only one that's actually worked...