> I gather you understand the topic, but I'm still left wondering: who is this for, and what will they do with it? 'Understand' is a big word. I've played arou

> I gather you understand the topic, but I'm still left wondering: who is this for, and what will they do with it? 'Understand' is a big word. I've played around with Idris (which is a Haskell-like programming language that supports Homotopy type theory as well). I have a grasp of the underlying mathematics but don't really understand the stuff deeply. Yes, I went on a bit of a rant and totally ignored your (totally reasonable) question. Theorem proving and proof checking are quite niche, both within computer science and mathematics. In computer science, the idea is that you can formally prove the correctness of computer programs to avoid software failures and have very robust programs. In mathematics, the ideal is to have 1. A universal language for proofs 2. A database of computer-verified results 3. Easy verification of new results It's a mighty interesting topic, and unfortunately, I've also found it quite difficult to get more than a shallow understanding of it.