I highly recommend just downloading and playing with a language based on type theory, such as Coq/Lean/Agda. I know Coq well, so I can recommend Software Founda

I highly recommend just downloading and playing with a language based on type theory, such as Coq/Lean/Agda. I know Coq well, so I can recommend Software Foundations and Certified Programming with Dependent Types. Write some simple proofs in one of those languages; for example you could try proving that addition of natural numbers is associative and commutative. At some point, it will start to click and you will feel like every other programming language you've ever used before is severely underpowered for not having dependent types. If you don't have experience with typed functional programming (e.g., Haskell/OCaml/SML), you will probably want to start learning one of those languages first. These languages won't really teach you type theory (at least, not the powerful kind of type theory that lets you do mathematics), but they will help you get comfortable with the syntax that type theory-based languages tend to use. I've written a Coq tutorial [1], but it assumes you already know functional programming. I'd appreciate any feedback on it if you decide to tackle it! If you want to dive into the theory, you can try reading Chapter 1 of the Homotopy Type Theory book. But many people find that book to be impenetrable, so it might not be what you're looking for (I personally love it). [1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutorial https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...