4 ms·

I doubt any of the "many" people that say that programming is more mathematically rigorous than mathematics are mathematicians. For mathematicians rigor is abou

I doubt any of the "many" people that say that programming is more mathematically rigorous than mathematics are mathematicians. For mathematicians rigor is about proof and they would never say that a discipline that usually does not involve writing proofs is more rigorous than mathematics. Maybe these people mean that formally verified programming is more rigorous than mathematics. That seems reasonable, but it is a tiny part of programming, isn't it? (Computer science, on the other hand, particularly the subfield affectionately called "theory", is typically mathematically rigorous.)

fizixer 9y ago
What I said is along the lines of 'every program is a proof' and what people like Philip Wadler say that we should treat propositions (essentially theorems) as types and programs as proofs. Now, where the mathematicians disagree-with/dislike such an idea has something to do with the question "If a program is a proof, what is the theorem?". Since we can have buggy programs, the norm rather than the exception, in my opinion the program is still a proof, just not for the theorem the programmer had in mind. When I say programming is more mathematically rigorous, what I mean is that a computer is way more precise at going through the program (a sequence of statements in a formally specified language) than a human-mathematician is at going through a proof (again a sequence of a statements in a formally specified langauge). In fact a computer never makes a mistake (unless there is a bug in the hardware or the compiler, i.e., something treated as an impossibility while programming). The mistakes are still at the human end (creating a proof/program for the wrong theorem/spec). A second, very strong, argument in favor of programming being more mathematically rigorous than mathematics: increasing reliance on computers for proof checking and assistance (not even including multi-terabyte proofs that would be impossible without a computer).
- catnaroek 9y ago
  (0) To view programs as proofs, you need to first view programming languages as logics. Alas, when (or even if!) you view any general-purpose programming language as a logic, you'll find out that it contains lots of junk theorems that nobody actually wants to consider theorems. (1) Don't conflate “rigorous” with “mechanized”. Rigor is a discipline that rules out invalid reasoning.
- omaranto 9y ago
  So you weren't saying that programmers are being rigorous when they write programs, but just that computers are rigorous when they execute programs? I guess I wouldn't really argue with that.
- tunesmith 9y ago
  It doesn't really mean much, though, if the working program (proof) corresponds to a theorem like "Given an Int, I can turn it into some other kind of Int", or "Given some sort of String, it's possible to turn it into a Boolean", or "Given an arbitrary input, I can yield some sort of arbitrary output". Those theorems are rather pointless. That's what most programs "as proofs" are like, where the value in them is in the side effects rather than their types. Now, when dependent types become more of a thing in the industry, maybe we can argue that our programs are getting more rigorous.

fizixer 9y ago

What I said is along the lines of 'every program is a proof' and what people like Philip Wadler say that we should treat propositions (essentially theorems) as types and programs as proofs. Now, where the mathematicians disagree-with/dislike such an idea has something to do with the question "If a program is a proof, what is the theorem?". Since we can have buggy programs, the norm rather than the exception, in my opinion the program is still a proof, just not for the theorem the programmer had in mind. When I say programming is more mathematically rigorous, what I mean is that a computer is way more precise at going through the program (a sequence of statements in a formally specified language) than a human-mathematician is at going through a proof (again a sequence of a statements in a formally specified langauge). In fact a computer never makes a mistake (unless there is a bug in the hardware or the compiler, i.e., something treated as an impossibility while programming). The mistakes are still at the human end (creating a proof/program for the wrong theorem/spec). A second, very strong, argument in favor of programming being more mathematically rigorous than mathematics: increasing reliance on computers for proof checking and assistance (not even including multi-terabyte proofs that would be impossible without a computer).

catnaroek 9y ago
(0) To view programs as proofs, you need to first view programming languages as logics. Alas, when (or even if!) you view any general-purpose programming language as a logic, you'll find out that it contains lots of junk theorems that nobody actually wants to consider theorems. (1) Don't conflate “rigorous” with “mechanized”. Rigor is a discipline that rules out invalid reasoning.
omaranto 9y ago
So you weren't saying that programmers are being rigorous when they write programs, but just that computers are rigorous when they execute programs? I guess I wouldn't really argue with that.
tunesmith 9y ago
It doesn't really mean much, though, if the working program (proof) corresponds to a theorem like "Given an Int, I can turn it into some other kind of Int", or "Given some sort of String, it's possible to turn it into a Boolean", or "Given an arbitrary input, I can yield some sort of arbitrary output". Those theorems are rather pointless. That's what most programs "as proofs" are like, where the value in them is in the side effects rather than their types. Now, when dependent types become more of a thing in the industry, maybe we can argue that our programs are getting more rigorous.