"A computer program IS a proof": Introducing rigor via programming

Question

This provocative essay

Igor Rivin. "Some Thoughts on the Teaching of Mathematics—Ten Years Later." Notices of the AMS, Jun/Jul 2014. (PDF download link).

suggests that a discussion of Igor's "principle":

A computer program IS a proof

might be worthwhile. I myself am very interested in conveying the notion of what constitutes a proof as early as possible in the educational system.

So given that most students have little understanding of what constitutes a proof by the time they reach college in the US (13th grade), what might be a good way to introduce that type of rigor earlier via a programming language, which effectively IS a proof, to quote Igor?

Answer 1

From the article:

For example, the student who wrote the program in the section “Source Code for a Modular Arithmetic Package in Scheme” had to have complete understanding of the Chinese Remainder Theorem, and his program is the Chinese Remainder Theorem in that, given some quantities satisfying the hypotheses of the theorem, it never fails to produce a quantity satisfying the conclusion.

This correspondence between program and proof (though far from perfect) allows us to make mathematics hands on...

So the principle in effect is only saying that "an algorithm to construct something of which a theorem states the existence, is a proof of the theorem".

I think that as mathematicians we would dispute that principle, and further dispute its out-of-context generalisation to the statement "a program is a proof", because it will lead to incomplete attempted proofs.

However, in terms of recognising a proof when you see one, a construction can certainly "be" an existence proof once you add the proof that the thing constructed has the properties stated by the theorem. So there's an aid to comprehension and possibly a useful rule of thumb here, it's just not actually true since, as the author says, there's no perfect correspondence between the program and the proof.

The imperfection of the correspondence can be illustrated by presenting the Python code:

n = int(input())
while n != 1:
    if n % 2 == 0:
        n /= 2
    else:
        n = 3 * n + 1
    print n

I propose that this clearly is not a proof of the Collatz Conjecture, please do not burst into rapturous applause ;-) Writing it didn't require any deep understanding of the conjecture, that gets me towards a proof. If the conjecture is true, then I've written a program that "given some quantity satisfying the hypotheses of the theorem, never fails to produce a quantity satisfying the conclusion", where the quantity it produces is a sequence ending in 1. Actually resource limits can bite, and I haven't checked whether the author of the article addresses that. The code I wrote is still not (on its own) a proof even that the conjecture is true for n smaller than some manageable bound.

If the conjecture is false then the program fails to halt on a counter-example, so is certainly not a disproof.

Furthermore, under normal circumstances we cannot call things "proofs" that don't even tell us whether the theorem is true or not! With modification my code could be used to produce a (ridiculously long) proof for small bounds, simply by generating all the sequences required. That leads to an argument about computer proofs that probably isn't really relevant to the thrust of Rivin's points, but I don't think that by accepting a computer-aided proof we have to accept that the program itself is the whole proof.

I think it's pretty typical to write programs that if the proposition is true can be fairly easily seen to produce the required quantity. For another example, one can and usually does write a program to factorise an integer, whose design and proof of correctness both rely on the fundamental theorem of arithmetic. Claiming the resulting program to be a proof of the theorem would be wholly circular.

Proving that my program produces the required quantity would prove the Collatz Conjecture, but a program on its own is not in general a proof that its outputs have particular desired properties. So by all means, programming might help introduce the notion of mathematical rigour if it's easier to ask and answer "how do we know this program does what it's supposed to?" than it is to ask and answer "what is a proof?". A proof is still needed, but the act of programming might make it much more clear what needs to be proved, and thus easier to write a proof and easier to see what a proof is.

In my example, it probably doesn't help, if only because computing the Collatz sequence is so simple that it's no easier to understand the question with the help of a computer. It's easier to explore what some sequences actually look like, that's about it. In other examples it might well help a lot, and perhaps the principle can encourage you to design programming tasks in a series of steps that ensure once the task is completed, the student has seen what they need to see in order to appreciate the proof.

I suppose that Euclidean geometry can and has provided the same introduction to rigour that programming can, since there too one can invent or be presented with a process that's observed to produce a certain result, and then challenged to relate this process to a proof of a proposition.

Answer 2

(By the way, I am in considerable agreement with Igor Rivin's premises and observations in that essay, and many of the in-principle conclusions, but might tend to doubt that the course of the juggernaut that is American culture and the concommitant educational system can be altered by the actions of a few quasi-rogue mathematicians in universities...)

So, first, my comment/reaction is that it's maybe not that a program is a proof, but the demonstration of correctness of an algorithm certainly is.

For context in regard to that article: I, too, have been frustrated by the intellectual state of undergrads, from perceptions of calculus, and I. Rivin's example of linear algebra, and even worse with "intro to abstract algebra". The latter was supposedly aimed at future high school math teachers, future actuaries, and math majors not going to grad school in math. After several experiments, it became clear that a majority of students could not only not write proofs or logical arguments or even sensible arguments, but could not reliably compose coherent paragraphs about very mundane actions.

Motivated by this situation (and other things), I cobbled together a "crypto" course and an "error-correcting codes" course to allow discussion of abstract algebra (and other important, basic mathematics along the way: combinatorical probability, a little linear algebra, finite fields, ...) with practical applications, and algorithm-oriented.

I still did ask students to narrate their execution of algorithms (with human-scale data). I had thought this would be a fair-if-minor challenge/goal.

I was to a considerable degree amazed that even very many "good" students could not, even with prompting, say what they had done, or why, even in very simple computations. "It's obvious." I tried to get them to write as though they were explaining something over the phone to someone who had no idea, but this seemed ... impossible.

That is, as artifact of the educational system in the U.S., people cannot reliably explain a process or algorithm. Observation suggests that a decade or so of not being required to explain things, but only to follows rules, does not beget narrative skill.

Nevertheless, I strongly hesitate to describe what even mathematicians would like from students as "proof". "Explanation", as a less stylized, more colloquial label, might be less polarizing and more explanatory to the general population.

But should kids be required to write programs? Maybe in pseudo-code. While I do understand Scheme and other dialects of Lisp and some other languages, I'd hesitate to insist on the "purity" of Scheme, as opposed to Python, for example. Not to mention the opportunities for killing time wrangling with syntax that is wildly different from English. No real point in that, unless we are wanting to inadvertently return to the (popular!) idea of mathematics as a discipline of adherence to semi-inexplicable "rules".

I was also dismayed to learn that many, many students believe that computers can do things that are even in principle impossible for humans, not merely on grounds of time or memory... but that they (computers) can compute trig functions and detect primes and do all sorts of things that no human could conceivably do. There is scant understanding that the atomic steps are perhaps even smaller for computers than for human-scale operations. Computers are magic?

So, yes, it would be good for U.S. students to learn that "proof" might mean, for example, explaining why an algorithm (whether executed by them or by a computer) produces useful outputs.

And then there're probabilistic algorithms (very relevant in crypto and in coding, thus to the internet, thus to everyday life...), which reliably disturbed many of the math majors... :)

Answer 3

I'm surprised not to see any mention yet of constructive type theory and computer proof assistants, in which a computer program is literally a proof and vice versa. For instance, if you wrote a program to compute the result of the Collatz function in a verified and termination-checked programming language like Coq or Agda, then it would be a proof of the Collatz conjecture. Conversely, a proof of the existence of an object in constructive type theory is, literally, an algorithm to compute that object.

I think computers have many roles to play in mathematics education. The coding of algorithms certainly has a place in education, but it seems to me that a more promising way to use computers to teach logical reasoning is to use a computer program that actually understands logical reasoning. Hence why I asked this question.

Answer 4

The first poster said that

it's maybe not that a program is a proof, but the demonstration of correctness of an algorithm certainly is.

I would modify this slightly (although I agree with the content of that claim). I think the phrase, in the context of the article, can be written as

Writing a program is equivalent to a proof.

In what sense? In the sense that getting a computer to correctly execute a function requires a total understanding, down to the last detail, of how that function works. In other words, making a computer find the GCD of two numbers has as its necessary and sufficient burden (besides fluency in the computer language, obviously) an understanding of how a method for doing so works (where "how" should convey both the "what" and the "why").

So from an educational standpoint, making students write programs to execute mathematical tasks is an excellent way to ensure that they will understand both how the method works (they wrote the code) and why the method works (they planned/problem-solved to come up with the idea behind the code). The why part constitutes the "proof" of the method - they could, in theory, give an adequate demonstration of the theorem if it was demanded of them.

Answer 5

Another thing worth noting is often times computers can only provide "approximations" of pure mathematical concepts and objects, simply due to the nature of the technology.

For example, in C and many other languages, a statement such as:

(1e200 + 1.0) == (1e200)

Will evaluate to true, simply due to precision loss in floating-point numbers. Did we just prove that $10^{200}+1=10^{200}$? We could easily construct a program that "proves" inductively that $10^{200}+n=10^{200}\>\forall\>{n}\in\mathbb{Z}$ (although we may reach limits of representable integer values), and another that proves the same thing not to be true by contradiction. We can "prove" that for any sufficiently large $n$, that $n+1=n$. And the only way to get to the bottom of it is to examine what is happening at the low level of bits and bytes and storage formats and digital arithmetic - all of which distract from the problem at hand.

Additionally, irrational and non-terminating numbers cannot be easily represented. For one common floating-point representation, for example, the non-terminating rational number:

1.0 / 3.0

Is actually:

0.3333333432674408000

There are plenty of other examples with numbers - integers wrapping around depending on the size of the variables used to store them, etc. I'm sticking to arithmetic because it's an easy example but there are much more subtle problems - memory limitations, incorrect usage of tools, design choices that affect results, bugs in underlying libraries, and also inherent limitations in using a discrete digital system to approximate continuous models.

So while it's possible sometimes to represent high level concepts in a program and have that program closely (or exactly) resemble a proper proof, many times it is not necessarily a direct proof of correctness because all of the lower level issues related to the actual technology can easily get in the way.

Much of this depends on the choice of programming language and other tools used as well. There are many different programming languages. For example, functional languages like SML and Haskell were essentially designed with induction in mind; programs written in those languages are often direct inductive proofs of correctness - whereas other languages can get bogged down in the technical details of the underlying system and subtle things sometimes nondeterministic, can ruin the success of a proof. In a language like Haskell, you can concentrate on the proof and not get bogged down in details.

Computers are useful tools just as calculators are useful tools, and programs can be used to aid constructions of proofs, but by no means are proofs in themselves. More often, you would use a proper proof to prove that the algorithms in the program were correct. There is simply too much "noise" -- other things to worry about -- involved in a computer program that take away from the strength of using it as a proof.

I wouldn't overlook the importance of programming, however. While programs aren't always themselves appropriate for proofs, teaching certain languages to a student (going back to the SML example) can, at the very minimum, teach a student a whole new way of thinking, and those skills can then be extended to constructing mathematical proofs. Learning a program language that is focused on induction most certainly changes the way a person looks at certain problems, and has the potential to add a few more great tools to somebody's mental tool set. Also some of these languages are great illustrative tools - for example, a calculator that solves algebraic equations and prints the steps is a good self-learning tool; just as an inductive proof written in Haskell opens itself up to examination and experimentation with instant and clear feedback.

Answer 6

I agree that the emphasis on calculation instead of understanding is a crime, and that skills in "liberal arts" areas (writing down a coherent description of a procedure, be it a recipe for jambalaya or pseudocode to compute the greatest common divisor) are extremely important, perhaps even more in technical areas (which tend to attract people who shy away from them) than otherwise.

On the other hand, equating "programming" with "proof" is a complete misunderstanding of both. Yes, in the hands of people like Dijkstra a program is a proof. Or perhaps better, Dijkstra's programs did include proofs, or had proofs written in parallel. Knuth's literary programming points in the same direction, write the program and the proof hand in hand, have the program typeset with the explanation for reading/checking by people, and compiled for running. But this is so rarely practiced that it gets lost in the noise. Most programming is (disturbingly) done by the "patch until it seems to work" technique. It isn't for nothing that Weinberg's Second Law states: If builders built buildings the way programmers wrote programs, then the first woodpecker that came along would destroy civilization.

Answer 7

I think one should consider two domains in parallel: writing programs, and writing test cases. If students became marginally proficient at both, I believe it would help crystallize their thinking mechanically. (It would also make them much better programmers.)

Unfortunately, it would not lend itself to the other kinds of thinking that should be present in people practicing mathematics, but it would be a good practice in developing rigor and abilities in refutation. For producing a mathematically literate individual, one will need some history, literature, and expository skills as well.

Gerhard "Make Minds Go Both Ways" Paseman, 2015.03.28

Answer 8

Here's what could realistically happen:

First, someone states a theorem T, which may be true or not.

Second, I write a program. I claim "if this program has output X, then the theorem T is true. If this program has output Y, then the theorem T is false. If the program produces output Z or doesn't produce any output at all in the time that I'm willing to wait, then I need to try harder".

Third, I run the program, which may output X or Y.

Fourth, the important step, if the program output was X or Y, is that I need to prove my claim from Step 2. So a computer program is not a proof. A computer program together with a proof what the output will be if the theorem is true or false, that's a proof.

It is quite easy for example to write a program that might demonstrate that the Collatz Conjecture is false (by finding an x where the Collatz sequence starting with x ends in a cycle); I have no idea how to even start writing a program that might demonstrate that the Collatz Conjecture is true. And I have seen many programs written by beginners where a proof would fail because of bugs in the program.

There is the minor problem that program + proof + output still require that the compiler compiled the program correctly, and that the hardware didn't make any changes to the calculation because of some cosmic rays and so on, but then any "normal" mathematical proof could contain errors that somehow everybody missed.

Answer 9

I don't think there is a need to begin with a programming language, because the language of mathematical proof already is like a programming language. Consider Algorithmic Problem Solving by Roland Backhouse.

The advantage of thinking about formal mathematics as a program (rather than the other way around) is that:

• the pedagogical approach is computer language agnostic and allows students to transfer "algorithmic problem solving" skills to any programming language, or formal mathematics notation;
• it allows students to realize that writing formal proofs is as creative an endeavour as writing a program, and more fundamentally so, because it is the basis of all programming!