242

Let me offer one reason and one misconception as an answer to your question. The main reason that it is easier to write (seemingly) correct mathematical proofs is that they are written at a very high level. Suppose that you could write a program like this: function MaximumWindow(A, n, w): using a sliding window, calculate (in O(n)) the sums of all ...


86

Humans can solve some instances of that problem efficiently, but there is no reason to believe that humans can solve all instances efficiently. Showing one instance that a human can solve efficiently does not imply that humans can solve all instances efficiently. Undecidable means "there is no algorithm that can solve all instances and that always ...


83

(I am probably risking a few downvotes here, as I have no time/interest to make this a proper answer, but I find the text quoted (and the rest of the article cited) below to be quite insightful, also considering they are written by a well-known mathematician. Perhaps I can improve the answer later.) The idea, which I suppose isn't particularly distinct from ...


60

Allow me to start by quoting E. W. Dijkstra: "Programming is one of the most difficult branches of applied mathematics; the poorer mathematicians had better remain pure mathematicians." (from EWD498) Although what Dijkstra meant with `programming' differs quite a bit from the current usage, there is still some merit in this quote. The other ...


52

Lamport provides some ground for disagreement on prevalence of errors in proofs in How to write a proof (pages 8-9): Some twenty years ago, I decided to write a proof of the Schroeder-Bernstein theorem for an introductory mathematics class. The simplest proof I could find was in Kelley’s classic general topology text. Since Kelley was writing for a ...


41

One big difference is that programs typically are written to operate on inputs, whereas mathematical proofs generally start from a set of axioms and prior-known theorems. Sometimes you have to cover multiple corner cases to get a sufficiently general proof, but the cases and their resolution is explicitly enumerated and the scope of the result is implicitly ...


28

They say the problem with computers is that they do exactly what you tell them. I think this might be one of the many reasons. Notice that, with a computer program, the writer (you) is smart but the reader (CPU) is dumb. But with a mathematical proof, the writer (you) is smart and the reader (reviewer) is also smart. This means you can never afford to get ...


24

One issue that I think was not addressed in Yuval's answer, is that it seems you are comparing different animals. Saying "the code is correct" is a semantic statement, you mean to say that the object described by your code satisfies certain properties, e.g. for every input $n$ it computes $n!$. This is indeed a hard task, and to answer it, one has to look ...


19

What is so different about writing faultless mathematical proofs and writing faultless computer code that makes it so that the former is so much more tractable than the latter? I believe that the primary reasons are idempotency (gives the same results for the same inputs) and immutability (doesn't change). What if a mathematical proof could give different ...


12

I agree with what Yuval has written. But also have a much simpler answer: In practice softwares engineers typically don't even try to check for correctness of their programs, they simply don't, they typically don't even write down the conditions that define when the program is correct. There are various reasons for it. One is that most software engineers ...


12

There are a lot of good answers already but there are still more reasons math and programming aren't the same. 1 Mathematical proofs tend to be much simpler than computer programs. Consider the first steps of a hypothetical proof: Let a be an integer Let b be an integer Let c = a+b So far the proof is fine. Let's turn that into the first steps of a similar ...


12

The remark is about one specific usage of Coq, namely formalization of programming language theory. Let us first make clear the distinction between synthetic and analytic: In a synthetic approach to a subject we say that there are things whose basic properties and structure are postulated in one way or another. We then study these things by relying only on ...


11

I like Yuval's answer, but I wanted to riff off of it for a bit. One reason you might find it easier to write Math proofs might boil down to how platonic Math ontology is. To see what I mean, consider the following: Functions in Math are pure (the entire result of calling a function is completely encapsulated in the return value, which is deterministic and ...


8

Nondeterministic automata would make perfect sense in a predetermined universe, because, in the sense it is used in computer science, "nondeterministic" does not mean "not predetermined." In particular, the acceptance criterion of nondeterministic machines is defined in terms of the existence of a path of a particular kind through the state transition graph....


8

It makes perfect sense. Non-deterministic automata and non-deterministic algorithms in general are useful in many situations. The best known situation is when one designs algorithms (or strategies or recipes or ..) and analyzes them. For example, an algorithm for computing the maximum element of a set of numbers will have a loop of the form "as long as the ...


8

There's another possibility: hypercomputation is not implementable in the real world, and is only an imaginary/theoretical concept. If this is the case, then there is no contradiction with the Church-Turing thesis. Of course, anyone can invent imaginary worlds where strange things are true. For instance, there's the computer scientist's Superman: not only ...


8

You are correct, a quantum computer defined properly: with a finite gate set and rational (you can relax this to algorithmic, but that can be bit circular) transition probabilities will get you only the computable (by a classical Turing machine) functions. Although it might compute them faster than a classical computer. To get a hyper-computer (something ...


7

Maybe I should make a more serious answer. First off: the unsolvability of the halting problem by "conventional" computing methods is a logical theorem. It is very simple to prove, and can be proven in almost any reasonable logical framework (that can express the problem). There are however two questions we can reasonably ask: What are the ...


6

Fundamental mathematical proofs does not amount to a real world application, designed to meet live humans needs. Humans will change their desires, needs, and requirements on what is possibly a daily basis in the realm of computer programs. What is so different about writing faultless mathematical proofs and writing faultless computer code that makes it ...


5

I can make some remarks that might help what you are trying to discuss. There have already been some mathematically well-defined computational models that can "compute" (define/recognize/etc.) uncomputable languages. For example, there are uncountable many languages defined by probabilistic finite automata with unbounded error [Rabin, 1963]. (The ...


5

Computer science addresses the mystery of computation (but not computers): what is computable, what is not-computable, how difficult it is to solve certain problems, when are programs correct, how can programs be effectively written, what's the best way of solving problem X (for many Xs), ...


5

No, you are confused. Turing machines and Hypercomputation are both mathematical models, and they are both consistent because we can build mathematical models in which all functions are Turing computable, as well as models in which hypercomputable functions exist. These are of course different models. There is no mystery about having a lot of mathematical ...


5

The Church–Turing thesis only purports to describe the types of processes that qualify as “computational”. It does not assert that “hypercomputational” processes are mathematically inconsistent. Most widely accepted formalizations of mathematics do allow us to define and reason about noncomputable functions. Some take “computation” to mean “process that can ...


5

I can't find the reference, but I think Tony Hoare once said something along the following lines: The difference between a checking a program and checking a proof is that a proof can be checked two lines at a time. In a word: locality. Proofs are written so that they can be easily checked. Programs are written so that they can be executed. For this ...


4

Looking at it from another angle, in a non-academic setting it often comes down to money. As the other posts assert well, Math is a single abstract specification, therefore a proof needs to work consistently within just that specification to be proven. A computer program may operate on many implementations of the abstract specification of math - that is to ...


4

I think that your reasoning is valid, but your input is not. Mathematical proofs simply aren't more fault-tolerant than programs, if both are written by humans. Dijkstra was already quoted here, but I will offer an additional quote. Yet we must organize the computations in such a way that our limited powers are sufficient to guarantee that the computation ...


4

It's not. Mathematical proofs are exactly as buggy by nature, it's just that their readers are more permissive than a compiler. Similarly, the readers of a computer program are easily fooled into believing it is correct, at least until they try to run it. For example, if we try to translate a mathematical proof into a formal language like ZFC, it will ...


3

We could ask whether it is more difficult in practice, or in principle, to write proofs or write code. In practice, proving is much harder than coding. Very few people who have taken two years of college-level math can write proofs, even trivial ones. Among people who have taken two years of college-level CS, probably at least 30% can solve FizzBuzz. But ...


3

I'll try to be original after all that great answers. Programs are proofs The Curry–Howard isomorphism tells us, the types in your program are the theorems and the actual code is their proof. Admittedly, this is a very abstract and high-level view. The issue you, probably, mean, is that writing a typical code is harder because it gets too low-level. In ...


3

As other answers have touched on in their answers(I want to elaborate), but a big part of the issue is library usage. Even with perfect documentation(as common as bugless code), it is impossible to transfer complete knowledge of a library to every programmer using the library. If the programmer doesn't perfectly understand their library, they may make ...


Only top voted, non community-wiki answers of a minimum length are eligible