IntelliJ’s take on dependently-typed languages, using HoTT (Homotopy type theory) for its foundations.

• Home page
• Tutorial

TODO List:

• Get through the entire tutorial.
• Get some understanding of the benefits of the underlying logic (HoTT) compared to what powers other theorem-provers.

Impressions

• Proofs are much more complex than I’d have expected, based on other dependently-typed languages.