I'm a little confused by the cutesy animal pictures on the first page... The only one that doesnt have some kind of lambda scribbled on them is the one that is directly lambda calculus, and I can't work out what some of the other symbols are even meant to be...

Related: https://github.com/AndrasKovacs/elaboration-zoo

The CoC implementation includes inductive types, so is this an implementation of CiC, the Calculus of Inductive Constructions, with the same proving power as Lean?

To the author: consider adding a dark theme to the code blocks. As-is, viewed on a system with a dark theme, these default to a really low-contrast light theme that's hard to read even without vision issues.

This seems to jump straight into type inference and bidirectional type checking, without a basic UNI-directional type checker

e.g. Featherweight Java (chapter 19 of TAPL by Pierce) is expressed with a simple unidirectional algorithm

And some of the languages in the PL Zoo - https://plzoo.andrej.com/

like https://github.com/andrejbauer/plzoo/blob/master/src/sub/typ... , although I am not quite sure

related thread: https://old.reddit.com/r/ProgrammingLanguages/comments/sq3z3...

---

I also think these statements are suspect:

We’re going to create minimal implementations of the most successful static type systems of the last 50 years.

As a result, many modern statically-typed languages have converged on a practical and elegant middle ground: bidirectional type checking.

I think what is missing in both statements is the word FUNCTIONAL.

e.g. Go, Rust, Swift, D, and Zig are modern statically typed languages, that are not functional. And I'm not sure if the authors would consider them "bidirectional"

I would like to see someone write about that. (I posed this query to 3 LLMs, and they mostly agree that those languages don't use bidirectional type checking; however I am wary of repeating AI slop)

e.g. this is a very good survey along those lines: https://thume.ca/2019/07/14/a-tour-of-metaprogramming-models...

---

This part also reminds me of Against Curry-Howard Mysticism - https://liamoc.net/forest/loc-000S/index.xml - https://lobste.rs/s/n0whur/against_curry_howard_mysticism

A deep insight has been unfolding since the late 1970s, a revelation that three immense, seemingly distinct realms of human thought are echoes of a single, deeper reality.