David Christiansen on Type Theory Forall

[janus]

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…

[simon]

I should probably use ML to make this summary but I don’t know these products well enough yet…

While AI might be helpful and reduce the amount of work, your summaries won’t be better. Doing them yourself shows that you have engaged with the content and have used some of your valuable time to write them.

[janus]

Now there is a follow-up episode: #39 Equality, Quotation, Bidirectional Type Checking

In today’s episode we talk about the story behind writing The Little Typer together with Dan Friedman, and we get more technical by talking about Equality, Bidirectional Type Checking, Quotation and Quasi Quotation.

Good stuff