I agree. It's kind of a focus thing. When I'm writing code, I do it because I want stuff to happen - in real life, in our physical reality. Any concept of code-as-a-proof is not even on my radar, unless I'd be writing life-critical software for NASA or a hospital, or something.

Here I also thing that 'Turing_Machine is both wrong in details and correct in the general point with their recipe example:

> Examining the measurements, timing, and the production chain doesn't tell you anything about whether the recipe is delicious or inedible.

You could, in principle, apply the knowledge of medicine, chemistry and biology, coupled with process engineering and wide-scale people studies, to construct a theory of tasty foods, which could lead to the situation in which you could evaluate any recipe on a theoretical basis. But getting to that state would require tons of up-front work to be done (some of which is being done for unrelated reasons, so maybe in the future a "food theory" will assemble itself) - and in the meantime, getting a piece of tasty food is done much faster and cheaper by finding the solution instead of deriving it. This search is done through iteration.

Similarly, in software, 99% of the time we find a solution, not derive it from first principles - because the former is much cheaper when we care about the solution, and not solving the entire general class of a problem at the same time.

The same is true for math. It is the same thing, because of the Curry-Howard isomorphism.

The reason for all the confusion is that programmers are already doing math. They just don't realize it and reinvent the wheels invented by the math community in the past century. It's a matter of semiotics.

Curry-Howard isomorphism does not mean the same practices that are performed in mathematics research must be applied to writing software.

Some aspects of language design are reinventing wheels invented by the math community. This is far from constituting the set of "writing software" or "software engineering".

Nah, I still think it's about different goals.

But assuming you're right, I'd like to know - what mathematical wheels am I reinventing in my dayjob of building UIs that let people click up some stuff that later gets put in business-specific XMLs?

Math, at least applied math, is not the goal, but the method. Programming neither is the goal, it is the method. Understanding that both are language to express the path is of the essence.

The XML as a vessel of human-knowledge is limited. Good intentions have brought it OWL/RDF, XML Schema, XSLT; examples where others before us have tried to extend the XML into the domain of semantics and algorithms. Nevertheless, it was found that, without an expressive type system, large and complex business domains cannot be modeled. Apparently, in order to model abstract business domains, we need a language that composes both high- and low-level with near invisible seams.

So, that click-your-XML-application might benefit from a reflective logic, enabling the user to explore the possible state-spaces. If your app uses relational algebra from DBMSs, it might be able to combine the relational algebra with the algebra defined by your schema's. The UI state-space and the XML schema might be an isomorphism, which helps prove completeness of your UI-builder implementation.

Above all, the mathematical way of thinking helps reasoning, communication and correctness. It might not be the only way or perhaps the way is dated. Nevertheless, ignoring math as a programmer, feels like ignoring music theory as a musician or linear algebra as a structural engineer.

We haven't been arguing that programming can't benefit from math.

> ignoring math as a programmer, feels like ignoring music theory as a musician or linear algebra as a structural engineer.

We're not ignoring math.

You're defining relationships between types through functions.