Hacker News Reader

Comment by gizi | Hacker News Reader

According to the Curry-Howard correspondence, all mathematical proofs are actually programs. This is normal. A proof is a series of steps, and if you unambiguously describe these steps, a computer will obviously be able to execute them. Furthermore, since Alonso Church successfully proposed a Turing-complete axiomatization based on just functions (even numbers are just functions), a computer program is clearly a mathematical object. An alternative axiomatization, Zermelo-Fraenkel, is based on sets. There is probably no better playground for sets than using a relational database. SQL is pretty much Zermelo-Fraenkel on steroids. In other words, large areas in math go into supporting the discipline of computer programming already. I do not believe that everybody would have to spend more time with areas in math for which no useful applications exist and that we are therefore unlikely to use in programs.

View on HN

All things that exist are mathematical objects and programs. Algorithmic information theory asserts that my cup of coffee is actually a program.

While mathematics is important to computer programming, for most practical purposes it is of limited utility unless you are inventing new computer science. Knowing how to use a relational databases correctly requires no formal set theory. Understanding how to build a massively parallel relational databases requires understanding the topological equivalents of relational operators, which is much more mathematical, but very few programmers design or build parallel databases.

Mathematicians need to be more open to accepting computer programs as results. It's one of the reasons we need better programming languages.

The problem with accepting computer programs as results is that they require much more scrutiny, as computer programs typically incorporate structures that are irrelevant to the result and yet may affect it (think memory leaks, etc). Mathematical proofs are a "pure" program, unencumbered by the technicalities of the real world.

As far as better languages for math, you'll enjoy this article + HN discussion: https://news.ycombinator.com/item?id=9572426

Those 'technicalities of the real world' are the things that lead to new and interesting mathematics. Maybe your 'whole number' concept doesn't properly model different kinds of measurement. Maybe you've got to iterate a couple time on the definition of 'smooth function' before you find one that's useful for modeling actual observations.

Mathematics is not unencumbered by the real world. It's just highly focused on specific classes of encumbrance. (If I put two marbles in an empty sack and poured out three, you can bet mathematicians would be interested in this new kind of arithmetical behavior, and try to model and explain it. Though talking to mathematicians, I get the impression they are so far up in the ivory tower, they think it isn't connected to the ground at the bottom!)

Our programs are not easily factorable. It is hard to separate different interactions across different problem domains. That's a problem of the language, not of the 'purity' of the program. Well, arguably. You could see it the other way, too, I guess.

> Knowing how to use a relational databases correctly requires no formal set theory.

Very true, I guess. But the other way around, someone who has used relational databases, will immediately understand formal set theory and find it absolutely trivial. Another example would be regular expressions. Anybody who has ever used them will immediately recognize what Kleene's closure is about and effortlessly deal with it. I think that this is generally the case. If you first solve problems with tools that embody a particular theorem, and if later on you read up on that theorem, you will find that theorem trivially simple. In other words, math and computer science are only hard, when you have never used them. Since formal education does things systematically in the wrong order, students tend to consider math and computer science to be hard.

Let me virtually shake your hand. I've always been successful teaching first from the concrete and then slowly abstracting - literally "pulling away" in Latin - as that's how I understand abstraction - it is the common ground between concrete things and therefore it was discovered from those things.

To then try and teach students first from the most "pulled away" concept possible to only in the very end try and meet them in the real world - I just never understood that approach. Like you said, the government curricula prescribe an approach that is backwards to what makes sense.

In Plato's Meno dialog, Socrates teaches a kid the abstraction called "irrational numbers" by having the kid draw triangles on the sand and then try and find the square root of 2. By playing with a concrete example (sqrt(2)) the kid learned the abstraction (that there are numbers that can't be shown as a fraction).

This backwards way of thinking we're stuck with today is so pervasive that one approach I was developing to teach monads - by first writing each instance separately and then later "pulling away" to try and see the bigger picture - was recently excoriated in the Haskell IRC channel for not teaching the actual abstraction.

The path is not the destination. You can't pull away (abstract) from nothing.

>someone who has used relational databases, will immediately understand formal set theory and find it absolutely trivial.

This is simply not true, you may understand the very basics of it, but by no means you will understand set theory and much less find it trval by just using relational databases.

What are you talking about? Programming is mathematics. Using a formal language to express solutions to formally defined problems is, by definition, mathematics.

Programming is not mathematics, except perhaps in the most narrow manner of recognizing that a syntactically formal language is likely used somewhere in the bowels of a solution.

However, formal methods and semantically formal languages are rarely used to arrive at the solution. Our mainstream programming languages are difficult to reason about semantically. The formality is mostly relegated to the grammar/syntax. Formal languages and methods might be used in rare cases to validate a solution after it was specified by other means. But those other means are usually a combination of art, engineering and a high-level imperative language.

You're recording your solution in a formal language. This is mathematics, by definition.

Any programming language that ever existed is a formal language. No matter how clumsy it is, it is always formal, otherwise it won't be possible to execute it. Even those stochastic languages are formal as well.

This is the fallacy of composition. (Human beings are mostly made of water. Therefore humans are water. Programming is about arranging numbers (code). Therefore programming is numbers. etc. )

Programming languages involved both syntax and semantics. Formal languages are concerned predominantly with syntax. Most programming languages do not have complete formal semantics grounded in logic. Pieces, sure. Most programming languages are a goulash of various formalisms mixed up with notions of aesthetics and mechanism.

Also, we're confusing code (which I agree is a mathematical construct, among other things), and a practice, programming. Almost no one programming is thinking purely in terms of mathematical logic. They're thinking about aesthetics, engineering constraints, user experience, timelines, procedures, libraries, version control, type systems, etc.

> Formal languages are concerned predominantly with syntax.

No. I'm using a broader notion of a formal language. Algebra, for example, is a formal language. One of the ways of defining a formal language is: "anything that can be strictly defined as a term rewriting system", and all the programming languages are fitting.

> Most programming languages do not have complete formal semantics grounded in logic.

They always do, otherwise their execution won't be deterministic.

A programming language implementation + semantics of the hardware and runtime library = semantics of a formal language.

> They're thinking about aesthetics, engineering constraints, user experience, timelines, procedures, libraries, version control, type systems, etc.

This is exactly how problems are solved in mathematics too.

If you want to extend even furthur into the metaphysics, it was Wolfram's "New Kind of Science" which (certainly not first) proposes that it's the computational universe that comes first given rise to the mathematical realism one.

>SQL is pretty much Zermelo-Fraenkel on steroids.

I didn't know SQL allows for infinite sets. In fact, most commonly used subset of SQL is non-Turing complete and decidable, while ZF is not decidable.

>all mathematical proofs are actually programs

This is not true. Only a subset is stated by Curry-Howard correspondence.

Reply on news.ycombinator.com