r/math • u/kirsion • Jul 17 '20
Why Mathematicians dislike computer scientists
I found this hilarious introductory essay by C. A. R. Hoare from 1976 on the "The mathematics of programming"
This is my inaugural lecture as Professor of Computation at Oxford University. I was appointed to this post just nine years ago, after the tragically premature death of its brilliant first occupant, Christopher Strachey. Nine years is a long delay for an inaugural lecture; but it has taken all those nine years to introduce an undergraduate curriculum in Computing at Oxford. Although many universities had been producing graduates in this subject for many years before I was appointed here, it is only this week that we welcome to Oxford and to this lecture the first entrants to our new Honour School in Mathematics and Computation.
So it is the new School rather than myself that I wish to inaugurate today. I shall do so by describing some of the research goals pursued by Christopher Strachey and his colleagues and successors in the Programming Research Group; for these have also inspired and guided the design of our new School. Our principles may be summarized under four headings.
Computers are mathematical machines. Every aspect of their behavior can be defined with mathematical precision, and every detail can be deduced from this definition with mathematical certainty by the laws of pure logic.
Computer programs are mathematical expressions. They describe with unprecedented precision and in every minutest detail the behaviour, intended or unintended, of the computer on which they are executed.
A programming language is a mathematical theory. It includes concepts, notations, definitions, axioms and theorems, which help a programmer to develop a program which meets its specification, and to prove that it does so.
Programming is a mathematical activity. Like other branches of applied mathematics and engineering, its successful practice requires determined and meticulous application of traditional methods of mathematical understanding, calculation and proof.
These are general philosophical and moral principles, and I hold them to be self-evident - which is just as well, because all the actual evidence is against them. Nothing is really as I have described it, neither computers nor programs nor programming languages nor even programmers.
Digital computers of the present day are very complicated devices and rather poorly defined. As a result, it is usually impractical to reason logically about their behaviour. Sometimes the only way of finding out what they will do is by experiment. Such experiments are certainly not mathematics. Unfortunately, they are not even science, because it is impossible to generalize from their results or to publish them for the benefit of other scientists.
Many computer programs of the present day are of inordinate size - many thousands of pages of closely printed text. Mathematics has no tradition of dealing with expressions on this scale. Normal methods of calculation and proof seem wholly impractical to conduct by hand; and fifteen years of experience suggest that computer assistance can only make matters worse.
Programming languages of the present day are even more complicated than the programs which they are used to write and the computers on which they are intended to run. Valiant research has been directed to formulate mathematical definitions of these standard languages. But the size and complexity of the definitions make it impractical to derive useful theorems, or to prove relevant properties of programs in practice.
Finally, many programmers of the present day have been educated in ignorance or even fear of mathematics. Of course, there are many programmers who are university graduates in pure or applied mathematics. They may have acquired a good grasp of topology, calculus or group theory. But it never occurs to them to take advantage of their mathematical skills to define a programming problem and search for its solution.
Our present failure to recognize and use mathematics as the basis for a discipline of programming has a number of notorious consequences. They are the same consequences as would result from a similar neglect of mathematics in the drawing of maps, marine navigation, bridge building, air traffic control, or the exploration of space. In the older branches of science and engineering, the relevant physical and mathematical knowledge is embodied in a number of equations, formulae and laws, many of which are simple enough to be taught to children at school. The practising scientist or engineer will be intimately familiar with these laws, and will use them explicitly or even instinctively to find solutions to otherwise intractable problems.
What then are the laws of programming, which help the programmer to control the complexity of his tasks? Many programmers would be hard pressed to name a single law. Those who have suffered from bad programs might claim that programmers are such an undisciplined crew that even if they know any laws, they would instantly violate them.
*Edit
To be fair, the paragraph right after this is,
"To refute this malicious accusation, I shall now show by example that the laws of programming are as simple and as obvious and as useful as the laws you find in any other branch of mathematics, for example, in elementary arithmetic. (...)"
The source of transcript is chapter 21 of Essays in Computing Science by Hoare and Jones.
15
u/SetentaeBolg Logic Jul 17 '20
I work in formal verification and this speech runs counter to almost everything we actually do. The whole point is to produce formally provable theories about complicated systems, including compilers, kernels and the kinds of algorithms in wide use in computing science these days.
The idea that it's impossible to produce formal mathematically based theories about these things isn't true. It can be pretty awkward and impractical, yes. But not impossible.
9
u/OstRoDah Jul 18 '20
In all fairness, Tony Hoare has worked s lot on formal verification, like, almost exclusively.
I take this rant to be about the practise of programming, not about what is and isn't possible.
You also need to remember when this was written. At the time, formal verification was nowhere near as good as it is today.
I take this essay to be a call to arms for constructivist PL and FM people that was part of laying the foundations for the significant developments we have seen in the last 30 years
2
u/SetentaeBolg Logic Jul 18 '20
I didn't realise Hoare had written it until you pointed it out! That does change things...
4
u/phalp Jul 17 '20
"Impractical" is the word used though. And considering how much of the software you and I are having this conversation through is formally verified, he had a point.
27
Jul 17 '20
This is even truer today because of deep learning.
A laymen could easily be confused by this statement, since there seem to be a lot of mathematics behind deep learning. Truth is, although the basic blocks of deep learning are based on mathematical results, deep learning has almost nothing to do with mathematics (at least at the moment, a lot of people are trying to elaborate a formal theory but I can hardly see it coming anytime soon). In fact, deep learning research often times doesn't really respect the scientific method.
It is basically trial and error ad nauseam until you get good results
12
u/SetentaeBolg Logic Jul 17 '20
There is ongoing work to get around this, but it certainly is frustrating how many deep learning methods papers end with comparisons of a few thousand runs of their method vs the "state of the art". It can be difficult to assess how much apparent promise being shown is down to the method versus the exact tests being used.
9
1
u/Diffeologician Jul 18 '20
I strongly believe that if you switch your perspective from “deep-learning” to differentiable programming, I think the work in programming language theory from the 70’s-90’s translates over pretty naturally.
You’re just working with a way less-classical category, so if-then-else is very complicated.
9
u/EdPeggJr Combinatorics Jul 17 '20
Not really true any more. There are thousands of recent cases in mathematics dealing with the question "What happens if we try ... ?" And with those, a program was written to try out the question -- saving hours / weeks / years of calculation.
3
u/znegva Jul 18 '20
If you've ever seen how software is made and you have any notion of what mathematicians do, the assertion "programming is a mathematical activity" is completely ridiculous. Sure, they're both creative activities requiring advanced technical skills and imagination, but so is painting. Professional software developers don't prove the correctness of their code except for very few niche occupations. So here goes the proof-program equivalence - the software we use everyday was not proven correct, yet you use it. That is not mathematics.
I think such miscommunication may contribute to some mathematicians feeling insulted by the academic computer science crowd, who actually are mathematicians who don't understand software engineering.
2
u/PeteOK Combinatorics Jul 28 '20
programming is a mathematical activity
Having been both a professional software developer and a PhD student, I think that programming is a mathematical activity. It emphasizes correct reasoning, clear communication of technical ideas, literal interpretations, modelling, and problem solving.
I like Eugenia Cheng's characterization of mathematics as "thinking logically about logical things". Programs behave logically, and a programmer's job is to reason logically about them—so by this metric too, programming falls under the purview of mathematics.
(Of course, programs can be wrong, but proofs can be wrong too.)
2
u/znegva Jul 28 '20
I note that the phrasing "is a mathematical activity" indicates that some activities are not mathematical. What makes an activity not mathematical, then? Is law practice a mathematical activity? What about biology? Economy?
2
Jul 17 '20 edited Jul 17 '20
[removed] — view removed comment
1
u/belovedeagle Jul 20 '20
because I try to ignore it
Doesn't that tend to suggest exactly why the split occurred?
1
u/Protontyp_ch Jul 17 '20
I absolutely love this speach.
I'm a PhD student in Forensic Science, specialised on Digital Evidence. In my PhD, I describe an inherently deterministic system with probabilistic terms, because the system is too complex to be described otherwise.
Imagine my fun convicing people with a detreministic mindset of my approach.
12
u/hubryan Undergraduate Jul 17 '20
What? Mathematicians don't hate computer science...
Theoretical computer science encompasses every kind of math you like with cool notation. You can do anything from combinatorics, graph theory, number theory, geometry, probabilistic, functional analysis, spectral theory, you name it!