Future of Coding is an online community with a welcoming, cooperative, and revolutionary spirit. We are unified in the belief that the common practice of programming is tragically less humane than it could be.

Future of Coding

Started reading this book to learn about Dependent Type Theory which is used in proof-assistant systems like Lean/Coq.

The author gave a talk at StrangeLoop which gives a good overview of the book: <https://www.youtube.com/watch?v=VxINoKFm-S4>

I need something that helps me _implement_ dependent type theory. So far, this book hasn’t covered that aspect.

<@U018S42NMMM> you might find this useful: <https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf>

I'm afraid I didn't get along well with _The Little Typer_. I don't know if there were issues in editing but I found it very difficult to follow the separate "voices" through the dialogue, which in the end made for a very frustrating reading experience. It's not that I dislike the dialog form (_Proofs and Refutations_ is a favourite of mine), but it just doesn't seem to work here. It's possible that if you're familiar with and get on with the other books in the family (_The Little Lisper,_ etc.) you might have a better time of it ... as always YMMV.