| > There are effectively two separate languages. Your type-level language and your term-level language. Computational Type Theory (CTT) blends the distinction b/w terms and types, and in fact C-H correspondence bears no consequence on CTT research. From a previous comment [1]: > I worry in dependently-typed languages that without preserving this distinction between types that have runtime-significance (Church-style) and types that do not (Curry-style), you lack an effective cast escape hatch. I think we've basically two categories of (turing-complete) programming languages: 1. Mainstream languages that use type systems for multiple purposes: operational semantics, compiler optimization, lightweight formal verification, etc, and provide casting escape hatches. 2. Languages where the type system's primary (and only?) purpose is formal verification, and there are no escape hatches. It's just that 1 and 2 are really meant for different domains. 2 is mostly used for high-assurance domains like aerospace, automotive, healthcare, blockchain smart contracts where formal verification is high priority and escape hatches aren't sought, hence not built-in. [1] https://news.ycombinator.com/item?id=22794925 |