3 ms·

> I'd say that CS was a superset of math, not the other way around. "Computer" is just the name we give to the whole class of physical tools we use to study inf

> I'd say that CS was a superset of math, not the other way around. "Computer" is just the name we give to the whole class of physical tools we use to study information. Then you'd be ignoring that a whole mess of math is not, in fact, computable (axiom of choice, law of excluded middle, etc). I think the problem is way too many "computer scientists" are pretty much software engineers.

tikhonj 11y ago
I am not ignoring any of that. Nothing says that you can't work with non-constructive logic in a programming language, or analyze non-constructive logics as programming languages. In fact that can be extremely useful although it's also, at present, difficult and not super common. The things you listed are extremely close to one of the foundational fields of CS, namely programming language theory. It's funny that you should bring up the law of the excluded middle because I learned a lot about it by studying PL theory: did you know that adding callCC to your typed lambda calculus turns it from a constructive logic system to a classical one? And that double negation translation is just a CPS transform which, at least for me, is a heck of a lot easier to reason about than proof theory directly? Everything in math is, at least in theory, provable. Provable in a discrete system (ie a formal logic) even if it's reasoning about something that isn't discrete. So there's nothing fundamental stopping us from doing exactly the same proofs in a formal system that a computer can understand. Oh, say, a programming language. Of course, with current technology, it's difficult from a practical standpoint, but there's nothing fundamental stopping us. And ideally it's something we should do to ward off errors and also to create proof artifacts that can be analyzed and manipulated systematically. Wouldn't static analysis for mathematical proofs be great? Or papers written as libraries so that relying on a lemma literally links against the proof it was first defined in. Seriously, if you dive into PL theory you'll see that the line separating CS from math doesn't really exist except as a social and technological phenomenon. (Lots of things are fundamentally possible but too difficult to do in reality, at least right now.)
- eastWestMath 11y ago
  Dude, I'm a grad student in categorical logic and I've worked with PLT. That's why I used them as an example. To formalize most math, the simply typed lambda calculus won't do, you need dependent types. But the logic used in math is almost always extensional, and type checking an extensional type theory isn't computable. Huge chunks of math, from analysis to chaos theory, are simply not computable.

tikhonj 11y ago

I am not ignoring any of that. Nothing says that you can't work with non-constructive logic in a programming language, or analyze non-constructive logics as programming languages. In fact that can be extremely useful although it's also, at present, difficult and not super common. The things you listed are extremely close to one of the foundational fields of CS, namely programming language theory. It's funny that you should bring up the law of the excluded middle because I learned a lot about it by studying PL theory: did you know that adding callCC to your typed lambda calculus turns it from a constructive logic system to a classical one? And that double negation translation is just a CPS transform which, at least for me, is a heck of a lot easier to reason about than proof theory directly? Everything in math is, at least in theory, provable. Provable in a discrete system (ie a formal logic) even if it's reasoning about something that isn't discrete. So there's nothing fundamental stopping us from doing exactly the same proofs in a formal system that a computer can understand. Oh, say, a programming language. Of course, with current technology, it's difficult from a practical standpoint, but there's nothing fundamental stopping us. And ideally it's something we should do to ward off errors and also to create proof artifacts that can be analyzed and manipulated systematically. Wouldn't static analysis for mathematical proofs be great? Or papers written as libraries so that relying on a lemma literally links against the proof it was first defined in. Seriously, if you dive into PL theory you'll see that the line separating CS from math doesn't really exist except as a social and technological phenomenon. (Lots of things are fundamentally possible but too difficult to do in reality, at least right now.)

eastWestMath 11y ago
Dude, I'm a grad student in categorical logic and I've worked with PLT. That's why I used them as an example. To formalize most math, the simply typed lambda calculus won't do, you need dependent types. But the logic used in math is almost always extensional, and type checking an extensional type theory isn't computable. Huge chunks of math, from analysis to chaos theory, are simply not computable.