https://www.typetheoryforall.com/episodes/haskell-lean-idris-and-the-art-of-writing-1
They talk:
- the Executive Director role at the Haskell Foundation
- Call-by-push-value
- getting started programming by booting into a BASIC prompt without a disk drive loaded
- GitHub - leanprover/verso: Lean documentation authoring tool, Scribble, LaTeX
- Mathlib is 1.4M LOC!
I should probably use ML to make this summary but I don’t know these products well enough yet…