[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.