Amongst some truly illustrious #programming languages and #proof assistants that sport a fully #dependent type system, #Lean now seems to be the firm favourite of mathematicians and programmers alike.
“Introduction to #Formal#Reasoning”, by Prof Altenkirch (Nottingham), is the most accessible text I have read on #logic for #CS undergraduates. The book uses #Lean theorem prover, to boot!
There are tonnes of great “intro” books and articles on Lean, all over the web. But most of them assume foundational knowledge in many subjects that most CS undies do not possess: formal logic, proof theory, recursion theory, functional programming, Hindley-Milner, Martin-Löf, Calculus of Constructions, and more. This makes it impracticable to use those “advanced intro” material to teach Lean to novice. And that is a missed opportunity, for it is vital to mould the undies’ malleable brains using FP, logic, Lean, and dependent type theory, before they become irreparably hardened into PP, due to excessive exposure to C++ and Python, as they are wont to do.
Altenkich’s book makes Lean, logic, and dependent types far less scary, and indeed enjoyable, for the kids.