[cubefox]

The book you mention is the opposite of "Logic for Programmers": it's abstract academic mathematics with zero code. (Except in the sense that constructive proofs are allegedly code. They are not, unless they are written in an actual programming language like Lean.)

[js8]

Yes, it's an academic work. But that's my point, somebody should popularize it among programmers, because the understanding of correspondence between a programming language and the metalogic we use to describe the problem (even when we talk to LLM for instance) has consequences how you approach programming.

"constructive proofs are allegedly code. They are not"

I disagree, what CHI shows is that specific language you choose matters only a little (as long as you stick to TC and have some means of compositionality).

I want programmers get to the point where they think of programming in a single unified language, of which different programming languages (and logics) are just expressions of (sometimes a bit more restrictive). I think it would enable metaprogramming (and formal methods) on an unprecedented scale.