@schindlabua: On a different note, regarding your series on type systems, specifically the very last part https://t3.at/blog/2025-12-24-type-systems-iceberg/ :

> Now.. we’re really reaching the boundaries of my knowledge here, but as I understand, not all theorems in mathematics are provable by constructive proofs, which is what the Curry-Howard isomorphism gives us access to. So there will always be mathematical truths that are outside the reach of any type system, that are provable under for example the set of axioms known as Zermelo-Fraenkel set theory with the axiom of choice (ZFC). ZFC is provably more expressive than λC or any other type system we can come up with, because the axiom of choice gives us access to non-constructive proofs.

I am no expert on type theory nor logic but I think there are a few errors here:

  - Curry-Howard is not restricted to intuitionistic logic / constructive type theories.

  - Type systems can be made arbitrarily expressive.

  - Non-constructive proofs exist in pure ZFC, too. They don't depend on assuming the Axiom of Choice. The core ingredient is the Law of Excluded Middle / proofs by contradiction.

Thanks! I might just reword that section or leave it out to not spread half-truths then. I'm really not very solid on either CoC or ZFC.