[linguae]

You brought up something interesting. I believe academic computer science originated from at least three cultures: pure mathematics (Church, Turing, Kleene, Dijkstra), electrical engineering, and psychology (Licklieder). I say “at least” since there may be other cultures I’ve overlooked. These three cultures have different views on programming: the EE-based culture emphasizes taking full advantage of the underlying hardware, the math-based culture emphasizes proof, and the psychology-based culture emphasizes human factors.

The challenge is reconciling these three views of programming: the holy grail is a programming language that is ergonomic and expressive, yet is also amenable to mathematical reasoning and can be implemented efficiently. I wonder if there is a programming language theory version of the CAP theory in distributed systems, where one compares performance, ease of mathematical reasoning about code, and human factors?