9 ms·

I'm a mathematician. Math shares a lot in common with programming. So much that it's easy to conflate the two. This caused me a lot of misery. The problem is t

I'm a mathematician. Math shares a lot in common with programming. So much that it's easy to conflate the two. This caused me a lot of misery. The problem is that the constraints around the development of mathematics are entirely different than software. Math is abstract, and there's no tolerance for incorrectness. A single inconsistency and we throw out the entire thing. Math is also not stateful, it costs nothing to throw out a theorem. Software is constrained in all directions: time, cost, performance, memory pressure, hardware compatibility, etc. For all that math shares with programming, practicing math shares very little with practicing programming. It was frustrating trying to design correct programs. My misery ended when I started thinking about software as biological systems. Software isn't constrained by correctness, it's constrained by fitness. Software decays if it's not maintained. It needs a metabolism: it must capture free energy from the environment and use that energy to increase its fitness (eg, making money in commercial software, or being useful to its maintainers in free software). It must reproduce, "infecting" new hosts. Software grows through accreted complexity and mutation, not up-front design. Software is unfit for survival outside of its ecosystem; as the ecosystem changes, it must adapt. Software has competition, predators, prey, symbiotes, and viruses.

nabla9 8y ago
Another way software is similar to biology and physical systems is leaky abstraction. Once you define something in mathematics, how you defined it does not matter. You can forget all irrelevant details. In the software irrelevant minute details make systems incompatible. As an example, Norbert Wiener defined ordered pair as: (a,b) := {{{a}, Ø},{{b}}} Hausdorff defined it as: (a,b) := {{a,1},{b,2}}, where 1 and 2 are two distinct objects different from a and b Kuratowski's definition (a,b) := {{a}, {a,b}} .. and there are many other definitions and variations, but still we have only one mathematics not many incompatible ones. Some mathematicians restrict them to subsets, but they don't create incompatible mathematics. If you do something similar in programming languages, you get two different structures you can't use interchangeably without transformation (it incompatibility starts from little endian vs big endian and ending ends with vi vs emacs).
- smilliken 8y ago
  It certainly feels like mathematics is better about leaky abstractions. It gets a lot more slack though because it's interpreted by mathematicians which can plug the leaks. For example, there's multiple formal definitions of integrals. They aren't strictly equivalent! But when we calculate an integral, we don't concern ourselves with the differences unless they are relevant.
- notduncansmith 8y ago
  This distinction seems false. You internally apply a compatibility layer, transforming for interchangeability and caching your computed equivalences. The same is frequently done in software.
- theaeolist 8y ago
  That is because mathematics tolerates informal proofs. Try to do formal mathematics (Coq, Agda, Isabelle/HOL, etc) and you will immediately see that it is not the case that {{a,1},{b,2}} = {{a},{a,b}}. Different definitions of "the same thing" are not "equal" but "isomorphic", and the isomorphisms are a bureaucracy that cannot be ignored -- unless you are doing regular, that is informal, mathematics and all this isomorphism business is just too tedious and 'obvious'. The problem with programming is that it is always fully formal. It may be lacking in rigour, but it is formal nevertheless. A compiler cannot process informal code (syntactically or semantically) and there is nothing it can classify as "obvious". Hence you need to spell everything out. Mathematics is like programming in pseudocode, that's why it's so neat.
  - gnulinux 8y ago
    > you will immediately see that it is not the case that {{a,1},{b,2}} = {{a},{a,b}}. This is true for the examples you gave i.e. Agda and Coq but this is not a theoretical restriction. As long as you can formalize equality with something like axiom of univalence, you can prove similar things (e.g. forall x, f(x) = g(x) => f=g which gives interesting applications like mergeSort = quickSort). Proving univalence constructively is pretty hard, but it's at least partially solved, e.g. cubic type theory can constructively prove univalence. Agda has a branch that has cubic type theory implemented, if you want to check it out. There is also an "official" implementation of cubic type theory by the team who wrote the original paper but it's a pretty lean programming language without even unification.
TeMPOraL 8y ago
I generally agree, though I have some issues with parts of the biological analogy. I believe there are two different meanings of "software" conflated here. If we look at software as a social phenomenon, then all the constraints you mention apply. However, if we look at software just as an executable artifact - it does not decay. Bit rot isn't real. Hardware can break down, but bits don't magically flip out of order just because the original developer went AWOL. This is important, because there seems to be this notion in our industry that everything needs to be updated and updatable all the time. But the truth is, unless someone purposefully screw it up (time-limited software, or Internet dependency), I can boot up my old machine and still do real work with decade+ old software.
- smilliken 8y ago
  Some types of software are much more resistant to rot than others. If your program has a URL, IP address, hostname, or file path embedded in it, those will eventually fail. If your program is compiled for (or designed for) a CPU architecture that isn't produced anymore, it's effectively rotting (even if you can run it in a VM, it's become second-class). If your program depends on OS functionality (practically all programs) that changes, it rots. If your program is designed to communicate with other processes, those processes will eventually become unavailable. One of my favorite pieces of software is the window manager Xmonad. It's written in Haskell and is very reliable. I can't recall ever experiencing an error. Yet regrettably, I'm going to have to find a replacement eventually because X11 is being obsoleted by Wayland. It's only useful because of its dependency on X11, which in turn is only useful because of the ecosystem of software around it. Speaking of decade old software, X11 is well over a decade old and doing well. It's evolved a good bit since, but is largely the same. In comparison though, the Pythagorean theorem was proven by the Greeks over 2000 years ago, and by the Chinese even further back, and is just as valid now as it was then. I get somewhat pensive when I consider that none of the software I've written will last remotely that long.
  - theaeolist 8y ago
    The analogy is a poor one though. This is nothing like rotting. A rotting thing changes, whereas here software stays the same but the environment around it changes. I know, no analogy is perfect, but this analogy is downright misleading.
notduncansmith 8y ago
Mathematics isn’t any less messy than software development - it precisely is software development. A theorem is a program we run on our wetware, and if a given wetware runtime doesn’t support the memory or time requirements for a theorem, it won’t run correctly. It’s also no less messy than anything else. Mathematics can still only offer us relative truth, and the differences between a theorem and a sharp stick are pretty superficial.
- smilliken 8y ago
  You're right. Mathematics is a program that runs in a brain, which is a wet computer. Subjectively, the distinction is useful. I'm never going to have a different brain, and I won't outlive my brain, so for all intents and purposes, my brain is an eternal constant. Theorems that ran on my brain once have accomplished their goal of convincing and never need to be run again. They are immutable.
- panic 8y ago
  > A theorem is a program we run on our wetware, and if a given wetware runtime doesn’t support the memory or time requirements for a theorem, it won’t run correctly. You can use a theorem without "running" it, though. The classification of finite simple groups took thousands of pages to prove; it would be pretty inconvenient if you had to read all those pages to use the theorem!
  - notduncansmith 8y ago
    Indeed, we usually don’t recompile the compiler every time we use it either.
jayd16 8y ago
Computer science (algorithms) and mathmatics are on one side of the line. Software development and engineering is on the other. Engineering is the art of ignoring perfection and eking out "good enough".
joe_the_user 8y ago
"Math shares a lot in common with programming. So much that it's easy to conflate the two." Well, I would like to point that both mathematics and computer science are human activities which occur on a substrate of determinant computational processes. Mathematics has a culture, history and set of standards which decide which among results of "proof processes" are "mathematically interesting" whereas Computer Science and Software Engineering engineering also have similar standards determining what's significant among determinant processes. Naturally, the two standards are distinct though actual results may occasionally intersect. Moreover, being "mathematically interesting" may make be a given item useful for computer programmers at times. Comprehensibility is important for our theories about programming despite programs having the usual requirement (unlike mathematical proofs) that they need a concrete manifestation. And both mathematics-the-human-endeavor and software-engineering-the-human-endeavor are full of metaphors that are false-but-useful. Computer programs don't literally decacy any more than mathematical truths have "inherent beauty" or exist in any ideal realm. But both metaphors are useful nonetheless. Also, the parent is confusing logical levels - programming is analogous to mathematical calculation whereas mathematics is analogous to computer-science or software engineering. Programs may be incorrect and calculations may be incorrect so many of distinctions are not germane to math/computer-science split (though the different ways programs are incorrect versus the ways calculations can be incorrect are relevant).
yaseer 8y ago
Well, we can actually _prove_ that mathematics and programs are isomorphic. (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...) You only get glimpses of that correspondence with procedural programming. It's much more apparent with functional programs though.
- Ar-Curunir 8y ago
  Doing mathematics is really nothing like software programming. Yes, there is an isomorphism between proofs and programs, but that doesn't mean much for the vast world of mathematics outside logic
  - marcosdumay 8y ago
    There are isomorphisms between any place of that vast world of mathematics and logic too. Math is also constrained by fitness, not perfection. Just take a look on the number of unproved conjectures we keep around. It's just that the Math community generally places more value on proofs than the programming, but it is a continuous, and there are more tolerant subcomunities of mathematicians and very intolerant ones of programmers too.
    - Ar-Curunir 8y ago
      I didn't mean that mathematicians don't write code; I meant that doing most mathematics isn't anything like doing programming, even when you're programming in Haskell. Just because two things are isomorphic doesn't mean they're used in the same way. For example, programming is formal but rarely rigorous; mathematics is the opposite.
      - marcosdumay 8y ago
        Most mathematicians do work that is very different from most programmers. Some programmers do work that is similar to most mathematicians, and some mathematicians do work that is similar to most programmers. Programming can be very rigorous, and mathematics can be very formal and not rigorous. There is a huge middle ground, sparsely populated between those.
nextos 8y ago
Computing as biology is the (temporary) perspective Alan Kay states in his famous quote: "We don't have a science of software engineering. Until we do, we should take advantage of late binding" [1] Once we are able to figure out things like model checking, program analysis, abstract interpretation and type systems, we will be able to do computing in a similar way to that of Mathematics. Or at least a bit closer, I think. [1] http://lambda-the-ultimate.org/node/531 http://lambda-the-ultimate.org/node/531
- gnulinux 8y ago
  This is a really bad argument imho. I'm an agda programmer, but only for hobby projects. You can do pretty much everything you listed: "model checking, program analysis, abstract interpretation and type systems" in agda, right now, this very day and some of these stuff is built-in (like dependent type system) or in the standard library. There even is a small industry built around proof automation. But it doesn't follow agda will solve software engineering. When it comes to engineering, it's also about constructing, not just about correctness. Everything you listed solves the latter while ignoring the former. I think the fundamental problem with software engineering is that it is a little too much like mathematics, to the point, the only way to be correct is to be as precise as agda, but, people who practice software engineering, again, just like mathematicians don't care to use this precise language. Just like a mathematician will never write his paper in agda instead of human language, unification will never by itself solve software engineering. Programs are written for humans, not for automated proof checkers, just like papers on mathematics are written for humans.

nabla9 8y ago

Another way software is similar to biology and physical systems is leaky abstraction. Once you define something in mathematics, how you defined it does not matter. You can forget all irrelevant details. In the software irrelevant minute details make systems incompatible. As an example, Norbert Wiener defined ordered pair as: (a,b) := {{{a}, Ø},{{b}}} Hausdorff defined it as: (a,b) := {{a,1},{b,2}}, where 1 and 2 are two distinct objects different from a and b Kuratowski's definition (a,b) := {{a}, {a,b}} .. and there are many other definitions and variations, but still we have only one mathematics not many incompatible ones. Some mathematicians restrict them to subsets, but they don't create incompatible mathematics. If you do something similar in programming languages, you get two different structures you can't use interchangeably without transformation (it incompatibility starts from little endian vs big endian and ending ends with vi vs emacs).

smilliken 8y ago
It certainly feels like mathematics is better about leaky abstractions. It gets a lot more slack though because it's interpreted by mathematicians which can plug the leaks. For example, there's multiple formal definitions of integrals. They aren't strictly equivalent! But when we calculate an integral, we don't concern ourselves with the differences unless they are relevant.
notduncansmith 8y ago
This distinction seems false. You internally apply a compatibility layer, transforming for interchangeability and caching your computed equivalences. The same is frequently done in software.
theaeolist 8y ago
That is because mathematics tolerates informal proofs. Try to do formal mathematics (Coq, Agda, Isabelle/HOL, etc) and you will immediately see that it is not the case that {{a,1},{b,2}} = {{a},{a,b}}. Different definitions of "the same thing" are not "equal" but "isomorphic", and the isomorphisms are a bureaucracy that cannot be ignored -- unless you are doing regular, that is informal, mathematics and all this isomorphism business is just too tedious and 'obvious'. The problem with programming is that it is always fully formal. It may be lacking in rigour, but it is formal nevertheless. A compiler cannot process informal code (syntactically or semantically) and there is nothing it can classify as "obvious". Hence you need to spell everything out. Mathematics is like programming in pseudocode, that's why it's so neat.
- gnulinux 8y ago
  > you will immediately see that it is not the case that {{a,1},{b,2}} = {{a},{a,b}}. This is true for the examples you gave i.e. Agda and Coq but this is not a theoretical restriction. As long as you can formalize equality with something like axiom of univalence, you can prove similar things (e.g. forall x, f(x) = g(x) => f=g which gives interesting applications like mergeSort = quickSort). Proving univalence constructively is pretty hard, but it's at least partially solved, e.g. cubic type theory can constructively prove univalence. Agda has a branch that has cubic type theory implemented, if you want to check it out. There is also an "official" implementation of cubic type theory by the team who wrote the original paper but it's a pretty lean programming language without even unification.

TeMPOraL 8y ago

I generally agree, though I have some issues with parts of the biological analogy. I believe there are two different meanings of "software" conflated here. If we look at software as a social phenomenon, then all the constraints you mention apply. However, if we look at software just as an executable artifact - it does not decay. Bit rot isn't real. Hardware can break down, but bits don't magically flip out of order just because the original developer went AWOL. This is important, because there seems to be this notion in our industry that everything needs to be updated and updatable all the time. But the truth is, unless someone purposefully screw it up (time-limited software, or Internet dependency), I can boot up my old machine and still do real work with decade+ old software.

smilliken 8y ago
Some types of software are much more resistant to rot than others. If your program has a URL, IP address, hostname, or file path embedded in it, those will eventually fail. If your program is compiled for (or designed for) a CPU architecture that isn't produced anymore, it's effectively rotting (even if you can run it in a VM, it's become second-class). If your program depends on OS functionality (practically all programs) that changes, it rots. If your program is designed to communicate with other processes, those processes will eventually become unavailable. One of my favorite pieces of software is the window manager Xmonad. It's written in Haskell and is very reliable. I can't recall ever experiencing an error. Yet regrettably, I'm going to have to find a replacement eventually because X11 is being obsoleted by Wayland. It's only useful because of its dependency on X11, which in turn is only useful because of the ecosystem of software around it. Speaking of decade old software, X11 is well over a decade old and doing well. It's evolved a good bit since, but is largely the same. In comparison though, the Pythagorean theorem was proven by the Greeks over 2000 years ago, and by the Chinese even further back, and is just as valid now as it was then. I get somewhat pensive when I consider that none of the software I've written will last remotely that long.
- theaeolist 8y ago
  The analogy is a poor one though. This is nothing like rotting. A rotting thing changes, whereas here software stays the same but the environment around it changes. I know, no analogy is perfect, but this analogy is downright misleading.

notduncansmith 8y ago

Mathematics isn’t any less messy than software development - it precisely is software development. A theorem is a program we run on our wetware, and if a given wetware runtime doesn’t support the memory or time requirements for a theorem, it won’t run correctly. It’s also no less messy than anything else. Mathematics can still only offer us relative truth, and the differences between a theorem and a sharp stick are pretty superficial.

smilliken 8y ago
You're right. Mathematics is a program that runs in a brain, which is a wet computer. Subjectively, the distinction is useful. I'm never going to have a different brain, and I won't outlive my brain, so for all intents and purposes, my brain is an eternal constant. Theorems that ran on my brain once have accomplished their goal of convincing and never need to be run again. They are immutable.
panic 8y ago
> A theorem is a program we run on our wetware, and if a given wetware runtime doesn’t support the memory or time requirements for a theorem, it won’t run correctly. You can use a theorem without "running" it, though. The classification of finite simple groups took thousands of pages to prove; it would be pretty inconvenient if you had to read all those pages to use the theorem!
- notduncansmith 8y ago
  Indeed, we usually don’t recompile the compiler every time we use it either.

jayd16 8y ago

Computer science (algorithms) and mathmatics are on one side of the line. Software development and engineering is on the other. Engineering is the art of ignoring perfection and eking out "good enough".

joe_the_user 8y ago

"Math shares a lot in common with programming. So much that it's easy to conflate the two." Well, I would like to point that both mathematics and computer science are human activities which occur on a substrate of determinant computational processes. Mathematics has a culture, history and set of standards which decide which among results of "proof processes" are "mathematically interesting" whereas Computer Science and Software Engineering engineering also have similar standards determining what's significant among determinant processes. Naturally, the two standards are distinct though actual results may occasionally intersect. Moreover, being "mathematically interesting" may make be a given item useful for computer programmers at times. Comprehensibility is important for our theories about programming despite programs having the usual requirement (unlike mathematical proofs) that they need a concrete manifestation. And both mathematics-the-human-endeavor and software-engineering-the-human-endeavor are full of metaphors that are false-but-useful. Computer programs don't literally decacy any more than mathematical truths have "inherent beauty" or exist in any ideal realm. But both metaphors are useful nonetheless. Also, the parent is confusing logical levels - programming is analogous to mathematical calculation whereas mathematics is analogous to computer-science or software engineering. Programs may be incorrect and calculations may be incorrect so many of distinctions are not germane to math/computer-science split (though the different ways programs are incorrect versus the ways calculations can be incorrect are relevant).

yaseer 8y ago

Well, we can actually _prove_ that mathematics and programs are isomorphic. (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...) You only get glimpses of that correspondence with procedural programming. It's much more apparent with functional programs though.

Ar-Curunir 8y ago
Doing mathematics is really nothing like software programming. Yes, there is an isomorphism between proofs and programs, but that doesn't mean much for the vast world of mathematics outside logic
- marcosdumay 8y ago
  There are isomorphisms between any place of that vast world of mathematics and logic too. Math is also constrained by fitness, not perfection. Just take a look on the number of unproved conjectures we keep around. It's just that the Math community generally places more value on proofs than the programming, but it is a continuous, and there are more tolerant subcomunities of mathematicians and very intolerant ones of programmers too.
  - Ar-Curunir 8y ago
    I didn't mean that mathematicians don't write code; I meant that doing most mathematics isn't anything like doing programming, even when you're programming in Haskell. Just because two things are isomorphic doesn't mean they're used in the same way. For example, programming is formal but rarely rigorous; mathematics is the opposite.
    - marcosdumay 8y ago
      Most mathematicians do work that is very different from most programmers. Some programmers do work that is similar to most mathematicians, and some mathematicians do work that is similar to most programmers. Programming can be very rigorous, and mathematics can be very formal and not rigorous. There is a huge middle ground, sparsely populated between those.

nextos 8y ago

Computing as biology is the (temporary) perspective Alan Kay states in his famous quote: "We don't have a science of software engineering. Until we do, we should take advantage of late binding" [1] Once we are able to figure out things like model checking, program analysis, abstract interpretation and type systems, we will be able to do computing in a similar way to that of Mathematics. Or at least a bit closer, I think. [1] http://lambda-the-ultimate.org/node/531 http://lambda-the-ultimate.org/node/531

gnulinux 8y ago
This is a really bad argument imho. I'm an agda programmer, but only for hobby projects. You can do pretty much everything you listed: "model checking, program analysis, abstract interpretation and type systems" in agda, right now, this very day and some of these stuff is built-in (like dependent type system) or in the standard library. There even is a small industry built around proof automation. But it doesn't follow agda will solve software engineering. When it comes to engineering, it's also about constructing, not just about correctness. Everything you listed solves the latter while ignoring the former. I think the fundamental problem with software engineering is that it is a little too much like mathematics, to the point, the only way to be correct is to be as precise as agda, but, people who practice software engineering, again, just like mathematicians don't care to use this precise language. Just like a mathematician will never write his paper in agda instead of human language, unification will never by itself solve software engineering. Programs are written for humans, not for automated proof checkers, just like papers on mathematics are written for humans.