I'm pumped cause this will popularize theorem provers and pump a lot of money into their development. There was that Stephan Diehl talk on the front page yesterday https://news.ycombinator.com/item?id=15582429 where he concluded that it's gonna be a while before see a language based on homotopy type theory.
He made a good argument. But these developments make me question whether crypto wont make them popular. This "early future" is kinda amazing.
I'm also waiting on Lean https://leanprover.github.io to introduce cubical type theory for HoTT. Version 2 of the language had HoTT based on the univalence axiom which was dropped in version 3. With cubical type theory the univalence axiom can be constructively proved and is no longer an axiom.
He made a good argument. But these developments make me question whether crypto wont make them popular. This "early future" is kinda amazing.