Are advances in Homotopy Type Theory likely to have any impacts on Rust?

71 points Dyson8192 61 comments

Basically the title. I’ve become interested in exploring just how much information can be encoded in type systems, including combinatorial data. And I know Rust has employed many ideas from functional programming already.

However, there’s the obvious issue of getting type systems and functional programming to interact nicely with actual memory management (and probably something to be said about Von Neumann architecture).

Thus, is anyone here experienced enough in both fields to say if Homotopy Type Theory is too much abstract nonsense for use in systems level programming (or really any manual memory allocation language), or if there are improvements to be made in Rust using ideas from HoTT?