5 ms·

I'm fighting through a book on formal logic at the moment, I never did a computer science degree, is it on the syllabus? It feels like this should have been the

I'm fighting through a book on formal logic at the moment, I never did a computer science degree, is it on the syllabus? It feels like this should have been the first thing I ever studied. I kind of got to it in reverse, data shuffling => everything looks like sql/pandas => everything is relational logic (read about minikanren, datalog, prolog) => lots of things are a surprisingly thin layer over formal logic. I haven't explored the idea but I read somewhere that type systems are close to unification (rust's typesystem is apparently very close ??). Interesting to see this article and realise that Dijkstra (God) was interested in logic too. Has anyone explored the idea that you write your program largely in logic, and that's your spec/typesystem, then you write the performance-relevant parts in a more procedural language, with either generative tests or some kind of proof system showing their equivalence?

auggierose 8y ago
Yeah, that's the basic idea of refinement based program verification. An example of that is: https://github.com/seL4/l4v https://github.com/seL4/l4v There are many programs which can be nicely specified with logic, and which could thus be treated this way. That we haven't build up the infrastructure yet to do this cheaply and routinely for those kinds of programs / libraries has various reasons. For example software engineers never doing a computer science degree ;-)
YorkshireSeason 8y ago
> 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...
- claudiawerner 8y ago
  >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. Unless it's a course in dialectical logic, or actually any other non-classical logic.
  - YorkshireSeason 8y ago
    I'm not sure what you mean. All formalisations of non-classical logic operate in the framework of first-order logic, in the sense that the informal meta-language in which the non-classical logics are explained in is traditional first-order logic, see e.g. [1]. I don't know what "dialectical logic" logic is. [1] Graham Priest, An Introduction to Non-Classical Logic
    - claudiawerner 8y ago
      Dialectical logic is a name given to describe the non-formal method apparent in Hegel's work, in which two opposing poles confront each other and progress towards a positive outcome. https://plato.stanford.edu/entries/hegel-dialectics/ https://plato.stanford.edu/entries/hegel-dialectics/
      - YorkshireSeason 8y ago
        The word logic has seen a marked shift (restriction) since Hegel's times: what Hegel meant by logic is no longer what we mean today by the term.
        claudiawerner 8y ago
        I'd question whether the people who talk about logic in analytic philosophy departments and mathematics have a monopoly on the usage of an ancient term and concept which has found immense value in non-formal contexts too.
        8y ago
deleted 8y ago
[deleted]
arethuza 8y ago
I'm pretty sure we did propositional and predicate logic in first year - UK CS course in the 1980s. Programming proving and synthesis was second year stuff, of a four year course.
MaysonL 8y ago
Back in high school (early '60s), I studied Suzanne Langer's Introduction to Symbolic Logic, and the fluency that gave me in Boolean algebra and bit-twiddling had me in good shape for many years.

auggierose 8y ago

Yeah, that's the basic idea of refinement based program verification. An example of that is: https://github.com/seL4/l4v https://github.com/seL4/l4v There are many programs which can be nicely specified with logic, and which could thus be treated this way. That we haven't build up the infrastructure yet to do this cheaply and routinely for those kinds of programs / libraries has various reasons. For example software engineers never doing a computer science degree ;-)

YorkshireSeason 8y ago

> 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...

claudiawerner 8y ago
>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. Unless it's a course in dialectical logic, or actually any other non-classical logic.
- YorkshireSeason 8y ago
  I'm not sure what you mean. All formalisations of non-classical logic operate in the framework of first-order logic, in the sense that the informal meta-language in which the non-classical logics are explained in is traditional first-order logic, see e.g. [1]. I don't know what "dialectical logic" logic is. [1] Graham Priest, An Introduction to Non-Classical Logic
  - claudiawerner 8y ago
    Dialectical logic is a name given to describe the non-formal method apparent in Hegel's work, in which two opposing poles confront each other and progress towards a positive outcome. https://plato.stanford.edu/entries/hegel-dialectics/ https://plato.stanford.edu/entries/hegel-dialectics/
    - YorkshireSeason 8y ago
      The word logic has seen a marked shift (restriction) since Hegel's times: what Hegel meant by logic is no longer what we mean today by the term.
      - claudiawerner 8y ago
        I'd question whether the people who talk about logic in analytic philosophy departments and mathematics have a monopoly on the usage of an ancient term and concept which has found immense value in non-formal contexts too.
        8y ago

deleted 8y ago

[deleted]

arethuza 8y ago

I'm pretty sure we did propositional and predicate logic in first year - UK CS course in the 1980s. Programming proving and synthesis was second year stuff, of a four year course.

MaysonL 8y ago

Back in high school (early '60s), I studied Suzanne Langer's Introduction to Symbolic Logic, and the fluency that gave me in Boolean algebra and bit-twiddling had me in good shape for many years.