Hacker Timesnew | past | comments | ask | show | jobs | submitlogin

Except the programs that programmers write very directly correspond to mathematics. The formal semantics of programming languages maps expressions in programming languages to mathematical expressions.

As such, all ordinary programmers are demonstrably writing mathematics - just with syntax, semantics, and applications that are unlike those of more traditional math.



I don't disagree with you, but I think your statement is roughly like: all ordinary composers are writing music theory, or all ordinary language users are doing linguistics.

Math is a way to add structure and understand the activity that programmers are engaged in. A lot of programming languages and computer architectures have been developed without the math in mind. There is still a lot of mathematical structure to be discovered in what an ordinary programmer does, I think. But yes, much of computer science, programming, etc feels very close to math, even compared to physics, linguistics, music theory, etc.


The difference is that programming languages are formal languages. They simply have a different syntax and semantics from traditional mathematics. The mapping between them is isomorphic.

> A lot of programming languages and computer architectures have been developed without the math in mind.

They're still formal systems. In a broad definition, they're mathematics themselves. In a narrower definition, they map isomorphically to more rigorous mathematics.


I look at https://en.wikipedia.org/wiki/Formal_system and I don't really see much resemblance to how mainstream programming languages are defined.

Some mainstream programming languages do not even a formal grammar for their syntax. Valid syntax is whatever is accepted by the parsing program. Much more commonly there isn't a formal specification of the semantics. The semantics are similarly defined by the implementation.

I think you might be arguing that the implementation is itself part of a formal system, involving the processor. I don't think I feel the same way. The CPUs operation can be described precisely in terms of rules, in the same way that Newtonian physics can, with the difference that digital systems are more robust to modeling errors. This is what the Strawberry picker example above, I believe, was meant to touch on. Just because math is used to model something doesn't mean the thing is math.

Some aspects of computational sciences feel like they are math. Other aspects seem like they're just modeled by math.


> The formal semantics of programming languages maps expressions in programming languages to mathematical expressions.

Which mathematical expressions do memcpy, fork, and putchar map to?


memcpy is trivially modeled as an operation on an underlying store. Such stores are a basic feature of any programming language semantics.

Putchar is easily modeled in terms of something like a state monad. In earlier semantics, such as the original denotational semantics, it was just modeled directly as a store that was threaded through a program, i.e. passed to every function.

Fork is modeled by process calculi.

If you think programming languages somehow can't be modeled by mathematics, you're essentially taking the position that they're doing something supernatural.


Library functions are not part of the formal semantics of programming languages.


Only a small fraction of programmers deal with math beyond basic arithmetic and simple Boolean logic.


The point is that by writing a program in a programming language, you're doing math whether you know it or not, because all existing programming languages have a direct, isomorphic mapping to mathematical expressions.

It goes well beyond "basic arithmetic and simple Boolean logic". One of the comment semantic descriptions of imperative programming languages involves a stack of monads representing the various effects that programming language support.

While most programmers may not be aware of this, they're still writing working expressions in a formal language which is equivalent to this.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: