If we attempt to apply Tao’s three stages -- pre-rigorous, rigorous, and post-rigorous -- to programming, something interesting happens: we find that the programming world is mostly stuck at the pre-rigorous stage because there is no widely accepted theory to guide practitioners to later stages. Yes, computer science has an accepted theoretical foundation, but computer science is not programming.
In programming, the closest I’ve seen to a widely practiced theory has come out of the Haskell community. There, you can see the beginnings of a theory in which programs are constructed out of formal building blocks like monoids and functors and where appeals to category theory and monad laws guide design decisions.
This is the most clear explanation for what I enjoy about the Haskell community I've ever read. I am utterly addicted to Conor McBride's [1] work as well since he's doing the incredible thing of answering semi-practical questions with deep dependent typing theory. I also think Gabriel Gonzalez's [2] writing has the right ideas as he tries to explain the feeling and heuristic of using categorical and functorial design while also writing a very beautiful library [3].
I also really can't get away without mentioning Edward Kmett[4], Conal Elliott[5], and Edward Z. Yang[6] for writing both blog posts and code expanding on the practical advantages of theoretical methods.
Having done a substantial amount of both math and programming, I feel like I can say that a start is all you will get, ever.
Most of the intuitions of programming are not provable and will not become provable, ever. I think I can back that up using the properties of the arithmetical hierarchy from Yu I. Manin.
I guess this is the order mathematics was taught in the authors university, in my experience with taking mathematics courses as part of a engineering degree, way too often there is no attempt at a "pre-rigorous" stage at all, as applications and intuitions are seen with contempt by the more formally-minded teachers. Vladimir Arnold's essay on this topic is a classic that I reread every few months for inspiration:
Richard Courant, the classic book of which is referenced in the article, remarks in the preface of one of his other books how the logical order of presentation of mathematical theories is much different from the order that works best pedagogically. I wish more educators would understand this seemingly simple observation.
As a teacher, the reason I teach with formality before allowing students to be informal, is that formality is training wheels.
Initially, the students do not know how to write a coherent proof. That is why we give them formal tools such as induction, and require them to write clearly, detailing their steps. When we do not do this, we see catastrophic lack of logical and coherent thought. Sometimes, this is the result of them not being able to _write_ their thoughts coherently, but more often, it is a results of their thoughts not _being_ coherent in the first place. Formality is used, partly, as forced coherency in writing, in an attempt to induce coherency in thought.
Once the students are able to write coherent proofs, sure, let them ride fast, let them "freestyle" proofs, with the confidence that what they're writing is what they intend to write, and with the skill to communicate concisely, clearly and unambiguously with informal language. If they can do it, more power to them. Often times, however, they need a lot of time with the training wheels, before they can ride fast and not fall disastrously.
Indeed, by the time that you get to an introductory analysis course in the US (a 300-level undergraduate course!), students generally are confused about what the givens are in a proof, and what exactly they are trying to prove, let alone getting from point a to point b. Most have not had to "prove" anything since 9th grade geometry, and are used to plug-and-chug solutions backed by geometric concepts stripped of formality. Still, I think that few students would get to this point without having those concepts, and if I get confused on a problem my first step is usually still to "draw a picture"! The two go hand in hand in my opinion, but due to the demand from the engineering departments for teaching mathematical solutions (I don't know the full history of how the curriculum developed but I suspect this and its associated budgetary reasons are a large part), half of the learning process is severely delayed.
I think you are talking about a different thing than I do. I have nothing against demanding some rigour in reasoning very early on in mathematics courses, what I am concerned about is the purely formal presentation of mathematical concepts, especially those that were first discovered by studying physical or geometrical situation and which naturally arise in such contexts. For example, is the formal epsilon-delta definition of a limit the best way to begin a calculus course? Yes, this is logically one of the basic building blocks of the theory, but what value does it have pedagogically for a beginning student? It is known that learning happens to a large degree via associating new concepts with ones already known, what can such a definition be associated with? This is carried out to extremes some times, I've seen introductory calculus books replacing sentences in natural language with formal-logic apparatus like quantifiers etc. and advertising it as some great pedagogical improvement.
Those are in my opinion excellent examples of courses developing intuition without sacrificing rigour:
I also love the books by Richard Courant for how they manage to explain the concepts in crystal-clear English writing, present both the applications and the theory, building up the rigour gradually.
You're confusing rigor with mathematical formality. Computing with equations that were taught to you formally, and solving mathematical problems rigorously are two different things. One of the easiest ways to tell the difference between the two modes of teaching is that in the former, you're taught a method and asked to apply. In the latter, you're frequently told the answer (though not always), and asked to find the method.
It is important to note that (in the Terry Tao's opinion) the 'more' comes only after being very thorough on the rigor and proofs,
He identifies three sequential stages in learning mathematics - the pre-rigor/intuitive handwavey stage, the rigorous 'axioms and proofs' stage and the final post rigorous stage (quoting from the article) .
'in which one has grown comfortable with all the rigorous foundations of one’s chosen field, and is now ready to revisit and refine one’s pre-rigorous intuition on the subject, but this time with the intuition solidly buttressed by rigorous theory. "
Many interesting thoughts on the transitions from one stage to the next. Great post.
The article & the associated comment thread have much to recommend them. But let's not glibly assume that "post-rigorous" ==> correct; much of economics can serve as a counterexample to that hypothesis.
I got out of mathematics (despite getting a PhD from a top department) because I felt that if all but a few dozen mathematicians in the world were shot, the progress of mathematics would not be much impeded, and I wasn't sure I would be in that several dozen. I did think I was that good in economics and related disciplines, but in that case there was a question as to what would get listened to. And so I wound up in a non-academic career ...
And before any of that, I got out of physics because it seemed boring. In the mid-1970s, that was a very fortunate decision. Going to grad school in math was somewhat about "Oops, I'm leaving my major, now what? Oh yes, I also finished a math major, and I can probably get into an excellent school and buy some time to decide what to do next ...."
Interactive theorem provers can quickly get you from stage 1 to 2.
If you are interested, [1] describes the experience of a professor teaching how to write correct and readable proofs about program semantics using the interactive theorem prover Isabelle/HOL.
Isabelle/HOL can make you learn fast because it allows one to get instant feedback on a proof. Proving things may then become surprisingly addictive.
The same tick-tock-tick pattern occurs in programming. There was a hacker koan about this I believe.
The apprentice is lax, undisciplined, and writes buggy code.
The journeyman sees all that he has wrought upon the poor world with his awful code, and immediately takes to applying every precept he can to produce rigorously engineered and stable code.
I leave it to the imaginations of others to perceive what might lay in the third step.
Good post! Generalizing the point, maybe a good description of sophistication is: using one's intuition in a natural way to explore the boundaries of one's knowledge, having previously refined that intuition by rigorous study and experiential learning. It's through an increasingly refined intuition about things within our horizon of knowledge that we're able to focus our conscious thought on the border of that horizon and expand it.
Three students were asked to evaluation the hypothesis "All odd numbers > 1 are prime."
The math major replied "3 is prime. 5 is prime. 7 is prime. 9 is ... NOT prime. The hypothesis is false."
The chemistry major replied "3 is prime. 5 is prime. 7 is prime. 9 is ... NOT prime. 11 is prime. 13 is prime ... The hypothesis is looking good, within experimental error."
The engineering major replied "3 is prime. 5 is prime. 7 is prime. 9 is prime. 11 is prime ..."
That's one way to cope when you're overmatched by rigor. ;)
I didn't get it either, but my guess: The engineering student took a literal view. You told him to evaluate the statement; you gave him a rule. If you say all odd numbers greater than 1 are prime, then so be it.
Well, suggested solution of this problem seems kinda backwards to me. I'd much prefer something along the lines of what Stephen Wolfram suggests - offload computation to computers in the first pre-rigorous stage, which may enable building of the foundation in a more rigorous manner right from the start.
Even at rigorous stage, offloading computation increases dramatically exposure to solutions and builds intuition faster by orders of magnitude.
Having written the following, I now wonder whether you meant something more specific by computation than I did, so I'm not certain whether my point is really a response. Could you spell out the details of your comment a bit more, and perhaps touch on the approach which Wolfram argues for?
* * *
Offloading computation only works when you understand what the computations are and why we do them. That's something that must be learned, it's not knowledge that springs fully formed into our minds as soon as we step into a classroom.
Carrying out computations thus gives us explicit and implicit knowledge of how the things we may eventually automate actually work. But it's also valuable because it trains us to compute in a precise and effective manner—a capability that remains useful later on. For instance, in logic it's often important to be able to carry out syntactic manipulations (e.g. into normal forms) in one's head, or even tacitly.
I'm sure there are plenty of examples from other areas of mathematics where computation is important, it's just that we do it so automatically that we don't think about it. Often I've found that students have trouble following proofs that take logically and computationally innocent steps without saying what's going on. Here I don't mean things like applying AC in the background, but just simple tricks like de Morgan's laws or taking the contrapositive. They have difficulty because they haven't taken those steps often enough themselves to have internalised them.
I just recall the Wolfram article and I seem to think it was pretty handwavey as to what/how things get offloaded (to Mathematica specifically of course). But I will say that at least half the homework of my Calc 1-3 courses was spent well past the "understanding" stage and more into "getting fast enough to do it on an artificial, time limited test situation" and basically memorizing pages of identities that I quickly forgot because they so rarely came up in my physics courses. This was pretty much the case with almost every math class since about algebra 1 in middle school.
And in particular I would like to hold up Electricity and Magnetism 2. Calculating the momentum of a magnetic field, in all but the most trivial case, takes a full sheet of paper: being rows and rows of 8 inch long equations as you carry out the tedious work of canceling terms; moving things in and out of square roots; and multiplying large polynomials together. It's all basic algebra stuff you learn in high school but it's a slog to work through and so time consuming that you actually lose track of the big picture and end up with very little better understanding at the end.
As far as I know that's why things like tensor and bra-ket notation had to be invented in the first place. Without a compressed notation the ability to get a correct answer to any interesting problem became less a question of knowledge and more a question of probability of transcription/sign flip errors.
not that anybody teaches sophmores tensor notation.
Unless you were truly exceptional, the "understanding" phase tends to get skipped in the first three calculus courses in favor of computation. Before you disagree read the following bullet points:
- What is the tangent line? How does it connect with the derivative?
- What is a limit. How is it used to make the above rigorous?
- What is the Fundamental Theorem of Calculus? Why, non-rigorously, would you expect it to be true?
That is not a random list. That's a list of the most important concepts taught in the first Calculus course or two. If you couldn't give a quick impromptu explanation of ALL of them, then you failed to master the key concepts. (Don't worry, most can't.)
To get to Terry Tao's formal math stage, you'd need to take proof-heavy courses such as real analysis.
I can, even 10 years later, not because I'm gifted but because I had good calc teachers who consistently covered and circled back on those points. I know what you mean though.
But what I mean is that 25th time you're doing an integral to ram home some trigonometric identity or working out a fourier series for PDEs it's not because anybody hopes that this is the time you get the epiphany it's because the teachers need something for the grade books and you need to be able to do it during a midterm.
Assuming Wolfram wasn't engaged in just an attempt to sell more mathematica licenses I would assume that was kind of his point. If you dump the most of the endless repetition on to maxima/maple/mathematica you could actually spend the semester on the concepts and proving them instead of focusing so heavily on the student's facility at algebraic manipulation.
Now having had to do everything by hand I have the sort of knee jerk reaction that "well I had to do it so they should do it too" but then I also remember that it sucked giant balls. As I see it is students definitely need pretty solid facility at doing this sort of shit and so we get the classic: "where do we draw the line" problem, which means I should probably not be counted as a proponent of Wolfram, so much as maybe a sympathizer (in this regard; fuck NKS).
*also while I take didn't real, I did get a minor in math which included Basic Concepts of Mathematics, or as I tend to remember it "that semester of not being able to divide because it's not defined over the integer set" but it was certainly a purely proof oriented course, and my numerical methods 1&2 were at least 50% proof based, I've done the formal rigor thing.
To this day I remember how outraged I was that on my final for Calculus 101 I derived from scratch an answer to an integration problem, then did the derivative and proved it was right on the final exam. Then the grader, upon seeing an answer different from the expected one marked it wrong.
I understand the grader was in a hurry, and the trig identity demonstrating that my answer was, in fact, equivalent to the standard one is not easy. But I had the right answer! And proved it was right, right there on the test!
I still remember the outrage. Over a question that did not matter then (I got an A+ in the course either way) or now.
What does this mean? For example I self-teach myself math at the moment, easy stuff like calculus. I'm still trying to get my head around it all. How can I offload computation to build up intuition faster? Any tips? (I love programming if that helps)
Particulary in starting calculus, after laying out the foundation of real numbers, exercises pretty soon start with determing limits, inflexion points, trends, and all.
Sure, play with those at first by hand, but try to plot and play with those functions in, say, Mathematica. Pretty soon you'll be able to intuitively "know" how any of the functions you could be thrown at exams should look like, which in itself is pretty usable skill.
Unrelated, I'd find it even more usable in physics, where solution guesstimate developed by exposure to numerous examples computationally solved can reliably indicate the correct solution as soon as you read the exercise or a problem.
Thanks for replying, I got to get back into Mathematica, its so different from "normal" languages. we use Matlab at uni a lot, but its not really the same at all.
Mathematics and proofs are a social process. Take a look at the classic paper by DeMillo, Lipton, and Perlis, Social Processes and Proofs of Programs and Theorems, available from several sources on the web.
Tao seems to be ignoring the common possibility that post-rgorous mathematical analysis makes mistakes, including proofs of (later realized to be) false statements.
The tick-tock analogy of a poster here makes more sense: rigor informs intuition, decreasing likelihood of error, and intuition generates hypotheses to be verified with rigor. But mathematicians I know don't think in intuition that can be perfectly converted into rigor.
In programming, the closest I’ve seen to a widely practiced theory has come out of the Haskell community. There, you can see the beginnings of a theory in which programs are constructed out of formal building blocks like monoids and functors and where appeals to category theory and monad laws guide design decisions.
It’s a start.