The Evolution of Lisp (1993) [pdf]
dreamsongs.com
dreamsongs.com
It is well-known that a majority of programmers dread mathematics beyond something basic like high-school math, sometimes even less.
What these programmers don't know is that a significant fraction of mathematicians (probably majority of them) who haven't been involved with programming, computers, computer algebra systems etc, have a similar dread about programming, in addition to the envy of programmers getting paid at much better rates.
It's also said by many, though without universal consensus, that programming is more rigorous than mathematics (here 'rigor' means mathematical rigor, nothing to do with everyday usage of the term).
When you start as a math major after high school, you take computational classes like calculus and linear algebra. Then you move on to theoretical stuff and "high mathematics" like real analysis and abstract algebra. Then, at an even more advanced level, you get into logic and foundations of mathematics, and at some point you get familiarized with the concept of constructive mathematics.
What I just realized is that programmers are essentially doing constructive mathematics (as well as logic, to a fair degree) all along, without realizing it, the moment they start coding!!! and yet the same programmers dread mathematics. That is funny (although not to say it makes it any easier for those programmers to learn all the rest of mathematics; IMO mathematics is still harder than programming as a discipline).
I think this is one example of many, I've found over the years but can't recall of the top of my head, where an expert of a given discipline is so encumbered by the "underlying machinery" of their field, that they fail to see that once they reach a higher level of abstraction, it sometimes becomes easier, rather than harder, if you forget about the details while working at that level, or you hadn't gone through the harder path to get there.
Another example being electrical engineers toiling through the difficult issues of power electronics, analog and digital design, computer architectures, instructions sets, only to find out that computer science people, who don't know all these things, have a much easier time working at the assembly language level, and those who don't even know assembly-language either, have no problem just sticking to a higher level language like ruby, javascript, and not worrying about or even aware of how the whole machinery works.
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.)
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).
(1) Don't conflate “rigorous” with “mechanized”. Rigor is a discipline that rules out invalid reasoning.
Look at how lambda calculus "functions" have been done in Java, who had OO and methods (~function) but had to reify lambdas in crude way. Proper math mindset allowed people to use these functions in a more abstract setting to do more with less.
Also after struggling with abstract algebra for long, I finally view these sorts of things as just another encoding of information as a dual of your problem. Modeling. It's a bit sacralized because either mathematicians are too much in love with their field or the rest of the world looks at it with ignorant eyes. It's beautiful, versatile and powerful, but approached the wrong way, it appears as more than it is.
In the end I believe that the two fields blend into one. I'm very curious to read HoTT for instance.
An operating scheduler can be regarded as a mathematical function, which chooses an element from a set. But then that choice has an impact on how the system performs under various conditions, which is pretty chaotic and doesn't follow in nice, obvious ways from that neat set-theoretic function.
Objects with Javascript code (34): [10, 16, 18, 22, 26, 30, 38, 44, 50, 56, 64, 70, 88, 94, 98, 120, 126, 132, 136, 138, 144, 161, 165, 167, 169, 174, 176, 180, 182, 184, 192, 214, 221, 225]
Recommend pdftops!