A ground up walk-through for using dependent types for formal proof. What I liked about this book is that it's presented more as mathematics than as computer science: you can work through the whole thing with pen and paper. It doesn't really have any specific prerequisites, just a general degree of mathematical maturity and exposure to proofs.
After reading this book, I felt capable of understanding how dependent-type-based theorem provers (e.g Coq and Lean) might be implemented.
> it's presented more as mathematics than as computer science: you can work through the whole thing with pen and paper
There's so much in software development that is shallow if you understand the motivation, or a key bit of context, because you already understand all of the hard parts. You "learn" a hundred things like this every week, mostly without trying, and there's a formula for helping people who get stuck: you find a concept that most people find trivial but a significant minority get stuck with, you figure out the bit of context that they're missing, you write a blog post or a Tweet or a HN comment supplying that bit of context, and bingo! Everyone who takes a few seconds or minutes to read it has an "aha!" moment and is suddenly, irreversibly enlightened.
Math has this kind of learning, too, but most of the effort in teaching and learning math concentrates on concepts that require a slower approach: the concepts that take some time to build up, or that require repetition for your brain to achieve the level of fluency needed for an idea to be useful. The "aha!" moment when it finally clicks is just the cherry on the top. It's a dramatic moment, but it has no value that can be separated from all of the prior work put in.
It's good to be able to recognize when you've been looking for the first kind of explanation for the second kind of concept.
I've been using Jupyter Book [0] at work to put together a cookbook for a market data analysis package, and am really liking it so far. I'm not a big fan of Jupyter's GUI editors for notebooks (and all the usual issues with .ipynb's under version control), but Jupytext is great and works quite well with Jupyter Book.
A ground up walk-through for using dependent types for formal proof. What I liked about this book is that it's presented more as mathematics than as computer science: you can work through the whole thing with pen and paper. It doesn't really have any specific prerequisites, just a general degree of mathematical maturity and exposure to proofs.
After reading this book, I felt capable of understanding how dependent-type-based theorem provers (e.g Coq and Lean) might be implemented.