Hacker News Reader

What math-backed theories? Why do they matter? Do you mean for the compiler team or for the users?

Hindley-Milner type inference and linear types (used indirectly for lifetimes) spring to mind.

Those are useful for compiler devs and language designers, not so much for the average user of the language.