> is [logic] on the syllabus? It used to be, but these days, most normal universities have de-mathematised their core CS curriculum, and logic is rarely taught

> is [logic] on the syllabus? It used to be, but these days, most normal universities have de-mathematised their core CS curriculum, and logic is rarely taught in any depth. If you are lucky it's a short few lectures on some introductory mathematics-for-computer-science Year 1 lecture. > this should have been the first thing I ever studied. In my experience as a CS prof at university, teaching logic at the start of a CS course will baffle 99% of students, and they will not see the point. At the same time, the top 1% love it. Note that as of January 2019, most programming jobs, including top paying FAANG jobs, don't require a substantial grounding in logic. Note that logic is deeply engrained in human thinking, we intuitively understand the meaning of terms like not, and, or, exists etc from early childhood on. The Kantian hypothesis here is that logic is part of the very fabric of our preception. So on some level, we don't need to learn logic as adults. What a logic course does it, tell us how to formalise logic. Moreover, by the Curry-Howard correspondence [4], (constructive) logic and programming are essentially the same thing, so one might argue that a computer science degree is basically a long logic course, but using a novel approach to formalising logic. > type systems are close to unification Yes, in the sense that type inference does unification. The most famous paper on type inference [1] is explicitly based on Robinson's famous unification algorithm [2]. User "dkarapetyan" in [3] even quipped: "Any sufficiently advanced type system is an ad-hoc re-implementation of Prolog. Once you have unification and backtracking you basically have Prolog and can implement whatever Turing machine you want with the type system." Relatedly, compilers for languages with advanced typing systems are sometimes quite slow (e.g. the old Scala compiler), and the cost of unification plays a big role here. As an aside, I recommend implementing the core type-inference algorithm in [1] for a toy language. It's simple, only ~100 LoCs in a high-level language, but it will really help you understand typing systems, and hence modern programming languages. Few things amplify your understanding of programming languages so much, for so little effort. > proof system showing their equivalence? Proving equivalence between programs is not computable (by easy reduction to the halting problem), and infeasibly expensive to do manually for non-trivial programs. Barring unexpected breakthroughs in algorithms (e.g. a constructive proof that P=NP), this is likely not to change in the next decade or two. [1] L. Damas, R. Milner, Principal type-schemes for functional programs. [2] J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle. [3] https://news.ycombinator.com/item?id=13843288 https://news.ycombinator.com/item?id=13843288 [4] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...