Re:Introduction to Functional Programming in OCaml
by kthielen on Thursday August 23, 2018 @12:27PM
(#17828566)
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.
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.