[kthielen]

Yes, there is only Curry-Howard and all PLs are just projections (to greater and lesser degrees).

Referential transparency, mutation, non-termination, coinduction, memory pointers, linear types, coroutines, continuations, blah blah blah. All of these things exist, and more.

Most PLs are biased in one way or another, many don't even let you reason formally about those things (or allow you to reason informally).

But at least if you're a working programmer, especially if you work to map an existing human domain to software, there's always the fixed point of Curry-Howard to hang on to.