4 ms·

Computer science should be called logic

1 points by learningstud 2y ago

learningstud 2y ago
At the very end of the video, the speaker quipped that computer science is not just about computers and an actual science doesn't have "science" in its name. The development of programming languages, compilers, SMT/MILP solvers, type theories, and proof assistants allude to the true nature of computer science, i.e., logic and its automation. It can be argued that computer science is even more fundamental than math, e.g., recursion/complexity, intuitionism/constructivism, linear logic, homotopy type theory.
- beardyw 2y ago
  > It can be argued that computer science is even more fundamental than math Perhaps "touches on more fundamental concepts than". Otherwise the fact it has the word "computer" in it and being only decades old makes being fundamental hard to support.
  - learningstud 2y ago
    Nowadays, logicians and type theorists find home in the computer science department instead of the math department. My whole point is to get rid of "computer" and "science" from "computer science."
ultra-boss 2y ago
We can apply logic to anything and everything. What makes computer science singularly deserving of this label?
- learningstud 2y ago
  Computer science studies and invents logic whereas the math community has departed from logic as a whole.
  - ultra-boss 2y ago
    Computer science "invents" logic? What do you mean by that? Are you familiar with the philosophy of logic and philosophical logic? Or formal semantics, which utilizes tools from the fields of symbolic logic and mathematics to generate (very precise) theories around the semantics of natural language expressions?
  - voidhorse 2y ago
    I would say that the working, active logicians study and invent logics, not the computer scientists, who work with the narrower field of objects known as models of computation.
    - learningstud 2y ago
      In reality, logicians and type theorists are employed in the computer science department and rightfully so. The whole field of computer science should upgrade with such influx of talent.
voidhorse 2y ago
Computation is a sibling (or maybe child) of logic, it is not a superset of logic. I like Wadler a lot and get that the Curry-Howard isomorphism makes it tempting to view them as the same thing, but logic is field of far vaster proportions and history. I think "computer science" is properly called computability theory. The proposal in the HN title is a bit like saying "calculus should be called mathematics".
- learningstud 2y ago
  Try programming in a proof assistant to see how inseparable computation and logic are. It gets more fundamental than the Curry-Howard correspondence when homotopy type theory enters the scene.

1 points by learningstud 2y ago

At the very end of the video, the speaker quipped that computer science is not just about computers and an actual science doesn't have "science" in its name. The development of programming languages, compilers, SMT/MILP solvers, type theories, and proof assistants allude to the true nature of computer science, i.e., logic and its automation. It can be argued that computer science is even more fundamental than math, e.g., recursion/complexity, intuitionism/constructivism, linear logic, homotopy type theory.

beardyw 2y ago
> It can be argued that computer science is even more fundamental than math Perhaps "touches on more fundamental concepts than". Otherwise the fact it has the word "computer" in it and being only decades old makes being fundamental hard to support.
- learningstud 2y ago
  Nowadays, logicians and type theorists find home in the computer science department instead of the math department. My whole point is to get rid of "computer" and "science" from "computer science."

ultra-boss 2y ago

We can apply logic to anything and everything. What makes computer science singularly deserving of this label?

learningstud 2y ago
Computer science studies and invents logic whereas the math community has departed from logic as a whole.
- ultra-boss 2y ago
  Computer science "invents" logic? What do you mean by that? Are you familiar with the philosophy of logic and philosophical logic? Or formal semantics, which utilizes tools from the fields of symbolic logic and mathematics to generate (very precise) theories around the semantics of natural language expressions?
- voidhorse 2y ago
  I would say that the working, active logicians study and invent logics, not the computer scientists, who work with the narrower field of objects known as models of computation.
  - learningstud 2y ago
    In reality, logicians and type theorists are employed in the computer science department and rightfully so. The whole field of computer science should upgrade with such influx of talent.

voidhorse 2y ago

Computation is a sibling (or maybe child) of logic, it is not a superset of logic. I like Wadler a lot and get that the Curry-Howard isomorphism makes it tempting to view them as the same thing, but logic is field of far vaster proportions and history. I think "computer science" is properly called computability theory. The proposal in the HN title is a bit like saying "calculus should be called mathematics".

learningstud 2y ago
Try programming in a proof assistant to see how inseparable computation and logic are. It gets more fundamental than the Curry-Howard correspondence when homotopy type theory enters the scene.