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}}}

    (a,b) := {{a,1},{b,2}}, where 1 and 2 are two distinct objects different from a and b

    (a,b) := {{a}, {a,b}}

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).

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.

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.

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.

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.

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.

But then what you said about software staying the same while the environment changes around it immediately made me think of evolution, Like any species that can't keep up with changes in it's environment, software that is not continuously updated to fit it's.

What do you think?

IMO again, this apply only along the social dimension of software. I can still boot up my decade-old computer and use decade-old software to do useful work (hell, many if not most factories do that all the time). I can be screwed over if I go on-line - either by getting pwnd, or by letting the OS update itself - but as long as I stay away from the Internet, the machine will keep working, and so will the software.

(Then again, 'smilliken turned out to be talking about much larger timescales - not decades, but centuries. There, no software artifact will survive, only its mathematical essence.)

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

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).

(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.

But when I program, then "trying to find any program that has a given type" rarely feels like the main problem I'm trying to solve. Depending on the program, I may want the program to do any of these things: run efficiently, conserve memory, have a good-looking and intuitive user interface, support multiple languages, be secure, be maintainable. If it's a web app, I want it to support multiple browsers. If it's a game, I want the challenge level to be just right. If it's a software instrument, I want it to sound good. You get the idea. So yes, there exists an isomorphism between programs and proofs, but I'm not really sure what to do with it, since the isomorphism doesn't preserve most of the properties I care about.

Formal specification in that sense isn’t enough to guarantee that your game is challenging—but it’s an engineering discipline that helps make sure your implementation is correct, and that you have clear and well-defined intentions.

Curry-Howard and dependent types is far from the only way to use logic for reasoning about programs!

One cool thing I’ve seen is using linear logic to make prototypes of games. Linear logic is good for expressing rules that consume and produce resources, in a way that fits very well with many game rulesets. Thinking of games as logical systems means you can ask questions like “is level 3 possible to finish starting with the items found in level 2?” (A proof could be a sequence of actions that start with those items and eventually reach the level’s end state.)

Logical reasoning isn’t the only aspect of software development, just like structural engineering isn’t the only aspect of building houses.

Homotopy Type theory also shows some deep connections between mathematics and programs, as the progress of the theory has bee characterised by building programmatic proofs _first_, to generate new mathematics. That's an inversion of the usual process.

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.

Programming can be very rigorous, and mathematics can be very formal and not rigorous. There is a huge middle ground, sparsely populated between those.

Engineering is the art of ignoring perfection and eking out "good enough".

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.

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!

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.