I would strongly recommend looking at “standard” dependently-typed theories and languages (or even proof assistants without dependent types), instead of trying to plunge into homotopy theory. Learning how dependent types work will be much more illuminating than trying to catch up on the algebraic topology. While the link between topology and formal logic is certainly interesting, I think you’ll be much better served by starting on the logic side of things.
Software Foundations is a well-known book / series of Coq programs for theoretical computer science. [1]
Lectures on the Curry-Howard Isomorphism[2] is my favorite (graduate-level) introduction to type theory and the lambda calculus, including the “lambda cube” and pure type systems.
Finally, while Type-Driven Development With Idris[3] is not at all “theoretical,” it is still an excellent introduction to dependent types and the idea of proof-as-program. It’s also the only book about a specific programming language I’ve ever read and actually enjoyed :)
Thanks for this very helpful comment which I've bookmarked for the links. Could I ask you for any more recommendations?!
I have background in standard undergrad math (linear algebra, calculus, real analysis, etc) and some basic undergrad CS, and I work as a software engineer (backend web stuff). However I've never really studied formal logic, or theoretical CS, or formal methods / verification, or type theory, and I was thinking of doing so. I enjoy studying math/theoretical things for its own sake, but I am of course also interested in techniques which might touch upon software engineering in practice.
Do you have any opinions on whether I am proposing something at all sensible for myself, and if so what sort of order to take things in?
Any recommended sources of exercises to work on (with solutions? seeing as I might well be self-studying)
Or lecture courses, or anything available online (even if it costs money)
Online communities you'd recommend for asking for help, e.g. with problems encountered in self-study?
And any more recommended books/lecture notes of course.
Disclaimer: I am not a domain expert in type theory and my background is algebraic combinatorics, not computer science. I also hate online courses, don’t like collaborative learning, and tend to read books and papers by myself. So I’m not a great source of advice for most people.
Unfortunately I don’t have many more suggestions that would be good pedagogically. Benjamin Pierce (who wrote Software Foundations) has another very famous intro book, Types and Programming Languages: https://www.cis.upenn.edu/~bcpierce/tapl/ which is regarded as a “Bible” of type theory for computer scientists. Note: I haven’t personally read this, but I have read the sequel, Advanced Types and Programming Languages. Both books have exercises and most exercises have solutions.
Simon Peyton-Jones wrote a very good book, the Implementation of Functional Programming Languages. It is old (1987), but free, a good read, and covers most of the “important” topics without assuming too much background: https://www.microsoft.com/en-us/research/publication/the-imp...
For formal verification - there are definitely better-qualified people than me. I found a lot of the source code to CompCert C (a verified C compiler) illuminating: https://github.com/AbsInt/CompCert However, it will be difficult to understand without doing Software Foundations first (I still find personally tactics-style proofs in Coq confusing and don’t like Coq as much as Idris or Agda).
I am very shy and can’t help you with the online communities :) The type theory subreddit is pretty active and they seem nice.
Great, thanks again! One more question: I imagine that it's not very important exactly what one picks as a beginner, but is Lean something which one might weight against Idris as something to start with, or would one get very different things out of learning about (and how to use) those?
Software Foundations is a well-known book / series of Coq programs for theoretical computer science. [1]
Lectures on the Curry-Howard Isomorphism[2] is my favorite (graduate-level) introduction to type theory and the lambda calculus, including the “lambda cube” and pure type systems.
Finally, while Type-Driven Development With Idris[3] is not at all “theoretical,” it is still an excellent introduction to dependent types and the idea of proof-as-program. It’s also the only book about a specific programming language I’ve ever read and actually enjoyed :)
[1] https://softwarefoundations.cis.upenn.edu/
[2] Available for free here (1 MB pdf) https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard....
[3] https://www.manning.com/books/type-driven-development-with-i...