From https://x.com/lexi_lambda/status/1486944837660250113

someone asked me in a conversation today to elaborate on why I have such an intensely negative opinion of SICP, and seeing as I took the time to type out my answer, I figure I might as well post it here, because it’s something people have often seemed surprised about

I have two major issues with SICP. The first is that it is a book about PL and has no business being used as an “intro to programming” textbook because it simply is not at all, and it doesn't even make sense in that context. But that’s really only a critique of how it’s used, not what it is, so I care about that point much less. My real issue with SICP is that I think the entire text is structured around an approach that is fundamentally an obstacle to understanding the ideas it’s trying to communicate. That is, SICP is about the way that we, as programmers, invent a language and imbue it with meaning through various techniques, and in particular the relationship between syntax and semantics.

Those are a really good set of ideas to teach programmers, but the problem is that SICP is based around this idea of “the metacircular evaluator,” which is a nonsense concept that doesn’t actually mean very much. The metacircularity comes from the fact that Scheme has a syntactic form called quote that can be used to acquire values of the concrete syntax tree as ordinary values in the programming language, through a particular mapping. But quote is actually very boring: it’s not meaningfully different from a data literal sublanguage, which many languages have, and in fact, it obscures the fact that the syntax is arbitrary and chosen by the programmer rather than something with inherent meaning. To me, this conflation of language and metalanguage is deeply at odds with an effective pedagogical approach to teaching beginners about the nature of programming languages, interpreters, and compilers.

I wondered how they adapted SICP to JS, since JS doesn’t have quote and while many of my broader complaints still stand, I think it’s funny how enormously better the JS version of this chapter is!

https://sicp.sourceacademy.org/chapters/4.1.2.html

I decided to bookmark this after seeing November 17, 2024 on HN: https://news.ycombinator.com/item?id=42164541

It is cool that the lambda calculus alone can express bools and ints. It is cool that you can encode data in the lambda calculus.

But I've recently learned that this is a dead-end for formal verification and theorem proving. So you can encode your data this way, but it seems to limit what you can do with this data, and so it is not quite universal in that sense.

It turns out that you need inductive data types? And they are easier to wrap your head around than Church encodings, in my opinion, anyway.

https://cs.stackexchange.com/questions/68808/why-church-encoded-types-arent-sufficient-to-express-inductive-proofs

For example, apparently you cannot prove that 0 ≠ 1 ?

https://cse.sc.edu/~pfu/document/talks/dtp-2013.pdf

<aside> ⚠️

Partial workaround

A stack exchange answer says

There is a result recently published within Annals of Pure and Applied Logic in which church encoded data are realizers of their own induction principle. In this system, the induction principle for natural numbers, trees, lists... are derivable. The core calculus doesn't have any datatype constructors packaged in. It starts at an extrinsic (curry style) System F adding 3 typing constructs: implicit product, heterogeneous equality, and dependent intersection.

https://www.sciencedirect.com/science/article/pii/S0168007218300277?via%3Dihub

Geuvers result does not apply to this calculus and is mentioned in the paper.

paper: "From Realizability to Induction via Dependent Intersection", by Aaron Stump

Friend tells me that this is a fringe type theory that is different from lean/coq/agda. It “doesn't support universes”. I don't know why universes are important, aside from avoiding, like, Russel's paradox.

</aside>

https://github.com/stepchowfun/proofs/blob/2f3392790c3d501c9ee428e10309d4a0bea70e66/proofs/type_theory/church.v

A demonstration (but not a proof) of why Church encodings of pairs don't support dependent elimination

https://x.com/lexi_lambda/status/1486944837660250113

You apparently can't proof “eta equivalence” (aka construct after destruct aka introduce after eliminate). If you try to prove it, you will run into trying to prove that two functions (in fact, dependent functions) are the same, even though they have different syntax. Defining