Post B0FDrwMOED3bINGv2m by AmenZwa@mathstodon.xyz
 (DIR) More posts by AmenZwa@mathstodon.xyz
 (DIR) Post #B0FDrwMOED3bINGv2m by AmenZwa@mathstodon.xyz
       2025-11-14T15:02:47Z
       
       1 likes, 1 repeats
       
       "#Functional #Programming in #Lean" (Christiansen, 2022) is the latest, and in my view the most accessible, introduction to academic #FP.Teaching #CS undergraduates how to wield their first functional language and their first theorem prover, simultaneously, is a monumental task. It is not something to trifle with, lest it sours the kids' taste for both. But Christiansen wrote this new, free textbook with that very purpose: to teach Lean as both the first FP and the first TP to FP novices. And it is undeniable that he succeeded in that goal.@d_christiansen co-authored (with Friedman) "The Little Typer", another eminently readable primer on an intricate subject: dependent type theory. And he was also an active contributor to Idris. He is presently at Lean FRO.https://lean-lang.org/functional_programming_in_lean/