Hacker News Reader

Comment by ukj | Hacker News Reader

The thing is - if Programming corresponds to Maths (according to Curry-Howard) what is really happening is Mathematicians and Programmers are disagreeing over language, not over substance.

Mathematics is a formal language. As such - it's part of the Chomsky hierarchy.

And if it's part of the Chomsky hierarchy - we can build parsers/interpreters/compilers for it. So why not standardise it all into a shared library?

That's exactly what Voevodsky did. https://github.com/UniMath/UniMath/tree/master/UniMath

As computer-assisted proofs become more and more popular, expect plenty of cross-polination between software engineers and Mathematicians.

Code refactoring. Unit testing. Managing a large, shared code-base. Fun times ahead.

View on HN

> As computer-assisted proofs become more and more popular, expect plenty of cross-polination between software engineers and Mathematicians.

Similar things were said in the 1950s and 1960s. I don't remember specifics but our lecturers told us that computer scientists back then thought that they could actually just mathematically express a program and there would be no need for a programmer.

The Vienna Development Method has been around for god knows how many years and have never caught on.

Saying that programming is like maths, is the same as saying cooking is like chemistry. Sure there is lots of chemistry going on in the food, but I doubt many chefs know or care about the chemical properties of organic compounds.

Additionally we actually did a course on VDM back in 2006/2007 and the lecturer said that he had only encountered one team that proved their program to be correct and it took them about a decade.

You could argue the code itself is the mathematical expression. But honestly as someone that has a very strong Maths background and moved to Software Engineering most software unless you are doing something very specific like a sorting algorithm a lot of code isn't really that algorithmic, you are in the vast majority of cases just expressing a set of business rules and that is in my experience is best described by Use Cases / User Stories.

For most businesses this is simply a waste of time. Getting developers to write tests is hard enough and businesses don't see the benefit until things start going horrifically wrong.

So, I remember once as a junior dev, I was asked to write a SQL script to get some data from some tables, etc. I wrote the script and it was taking for ever to run. I scratched my head, had a close look and it was obvious that my script was running in quadratic time (plus, you know- expensive joins and stuff). I rewrote it to run in linear time and, hey, presto- the job was done in a flash.

That is how programmers use maths to do their everyday work.

Note that I don't mean you need to know that what you're doing is asymptotic analysis and so on to optimise your code when it gets bogged down in unnecessarily expensive compuations, but even if you don't call what you do what it is formally known as, you are still doing that thing. And that thing is called "using maths".

It always boils down to use-cases.

Ultimately, what formal verification gives you is a guarantee of structural correctness, but not behavioural correctness. Whether a program behaves as intended or required is still a task for humans. Garbage in - garbage out.

Whether structural correctness is a requirement is a function of the software's criticality and purpose.

You probably don't need it for your blog...

There is one critical FYI. If you require formal verification of your code you have to give up Turing-completeness. https://en.wikipedia.org/wiki/Total_functional_programming

This is a facetious comment that others have made: https://twitter.com/pigworker/status/913454521610842114

One issue that it glosses over is that in mathematics, the object of study is a-priori truths (and mathematicians are usually Platonists). I would express this as saying that math is interested in knowing what's true. So obviously it is applicable to proving things about programs. So far so good.

But programming involves a lot of work which could be described as a-posteriori. As an example on dictionary.com puts it, "an a posteriori argument [...] derives the theory from the evidence". Programmers are designers, wrestling sense out of complex and sometimes poorly expressed specifications, requirements, and realities. This doesn't map onto mathematics: it's neither (in Gowers' terms) theory building nor problem solving, because mathematical theory building is an a-priori business dealing reflexively with mathematical tools, not with theories of the outside reality. A typical large software system is an unwieldy, organic thing, to which mathematically formulated theories apply in the same way as they do to biological organisms. Sometimes math can describe aspects a complex system well, but it can't tell you how to build it, any more than it can tell you how to build the Parthenon.

A-priori truths are called axioms.

In the context of the Curry-Howard isomorphism you don't "prove things about programs".

Programs ARE proofs. Not all programs, mind you. You need to be using a dependently-typed language like Agda, Coq or Idris.

The link in my post to the UniMath project is a bunch of codified proofs to various theorems in Category theory, Topology, Combinatorics etc.

I don't agree that a-priori truths are limited to axioms—it's a much larger category of "necessary" truths. A theorem which has been proved is an a-priori truth.

Sure, programs are proofs in the context of Curry-Howard. But not necessarily proofs of what you want them to prove.

If it has been proven from your axioms (really down from the axioms!) then you can add it to a library of statements you 'know' (or in the case of your axioms, assume) to be true.

More succinctly: The thing you want proven is a proposition.

A proposition is a type. Writing the algorithm which implements the type is the same as proving it.

https://ncatlab.org/nlab/show/propositions+as+types

A theorem is a consequence of a set of axioms. By definition.

It may be an a-priori truth in the context of the particular proof you are working on, but a-priori your theorem there is always an axiom.

Wanting to prove that X is a theorem of a-priori truth Y is the same thing as writing the algorithm for f: Y -> X

Thanks for explaining what I was trying to say much better than myself.

...maths is not a formal language by any stretch of the imagination. I think about the best definition one can give is maths is what mathematicians do, and maths notation is what one mathematician writes down to communicate mathematics to another mathematician.

It's circular in about a dozen ways but that is as it is IMO.

I'm fairly certain that Hilbert would disagree with you:

https://en.wikipedia.org/wiki/Formalism_(philosophy_of_mathe...

In particular, most modern mathematics can be formalized within first-order logic with the ZFA axioms:

https://en.wikipedia.org/wiki/First-order_logic

https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t...

As a concrete example, the metamath project has formalized (and formally verified) huge chunks of mathematics:

http://us.metamath.org/mpeuni/mmset.html

Certainly there are aspects of mathematics which are not formal (beauty, parsimony, elegance, clarity, geometric intuition, etc.) but saying math isn't a formal language is like saying chess doesn't have rules.

He's not saying mathematics doesn't have rigorous foundations.

Betrand Russell's Principia Mathematica is computation. But math textbooks/papers are not like this. They share insights, opinions, and metaphors, and frequently explain things in non-rigorous terms, although these are not substitutes for proofs even though proofs for something given a non-rigorous explanation may not appear.

In less heavily proof-read contexts, such as in discussions or a class room, it's not uncommon for mathematicians to be pretty free-wheeling with their notation, and leave it up to context and intuition to figure out what an individual symbol means at a given time. And it wouldn't be a faux pas, or sign of a lesser mathematician or anything like that.

These things can be valuable and in some sense are a part of mathematics.

Although the end results of mathematics can be distilled into formal computations, it's far too reductive to say that's all mathematics is.

The exact same thing can be said about any human dynamic where the objective is to teach.

The end-goal is to make the material accessible to the learner by connecting it some pre-existing human intuition or experience, thus providing the learner with a vocabulary to express their thoughts.

The important question is how are the vocabularies (both formal and informal) produced by Mathematics different from the vocabularies produced by Computer Science when both fields are working on the same real-world problems?

And if the two vocabularies are of equal utility - do we really need two different tools for the same job?

Computer science and mathematics do not work on only the same problems or produce the same results, except for the parts which overlap. Unless you're attributing results by automated theorem provers as results in computer science?

The point of mathematics being expressed in these ways isn't just teaching. Mathematics may be abstract, but it is still fundamentally abstracting patterns which arise from the human experience (for the most part). Tying mathematics back to human experience is an important aspect of the discipline. But another important reason is to engender further research and advancements.

What you're saying is exactly asking whether programs can replace programmers, since you can design a program which generates programs.

Mathematics and computer science are human disciplines with results whose purpose is to find results which are of interest to humans. At this point we are able to sometimes verify theorems and occasionally prove a theorem automatically. But ATPs are unable to write comprehensible proofs, tell what corollaries may be of interest, or to autonomously build off of theorems in directions which would interest us. At this point they are not necessarily able to prove theorems in reasonable time frames.

Furthermore the results produced by vocabulary are not just theorems. High quality proofs are just as valuable. They tell us why things are true in ways which are significant or profound. Although the 'why' is not necessarily useful, it is still of interest to mathematics.

Perhaps ATPs will be able to accomplish all this eventually. But currently they don't provide the same utility as mathematics.

I think you are missing the point.

Solving a problem using mathematics is EQUIVALENT to solving a problem using computation (which is a silly truism, because your mind is a computer).

They are two different mind-instruments, two frameworks for thinking and thinking about thinking. They are functionally identical

What you can do with one - you can do with the other.

Because Mathematics can only prove things up to an isomorphism. And Curry-Howard is an isomorphism.

Whether any particular solution can be automated is not my point at all.

My point is that when a human solves an abstract problem - they express the solution in language.

Some humans speak Mathematics. Some humans speak Python.

The divide between Mathematics and Computer science is cultural, not grounded in utility.

Hence why - I would love to see some unification.

>I'm fairly certain that Hilbert would disagree with you

Hilbert failed. Besides actual mathematics are not done in a formal Hilbertian way...

Where Hilbert erred was looking for foundations in first-order logic. Univalent foundations are laid on high-order logic.

It's the distinction between top-down and bottom-up thinking.

If you are into philosophy/epistemology - it's somewhat of an attempt to shift Mathematics from foundationalism towards structuralism.

I recommend this video: https://www.youtube.com/watch?v=O45LaFsaqMA

Hilbert's dream of Metamathematics has sort of come true in the form of homoiconicity in programming languages.

What mathematicians DO is computation.

What a mathematicians WRITE is a formal language used to express computation.

Manipulating mathematical expressions has a name. Symbolic Computation. https://en.wikipedia.org/wiki/Computer_algebra

One can view it as "language" at multiple levels.

In a computer language, there is a lexical level, and then there is a slightly deeper syntax level. Beyond that, there are levels of language, too: JSON or XML documents can follow one schema or another, for example. This schema defines a language on top of the JSON or XML language. (And you can do the same thing with any other data structure.)

In math, the same sort of levels exist. At the most superficial level is the notation. At that level, I don't think mathematicians use formal language. They're free to invent a notation or even misuse a notation in a proof. There are no absolutely fixed rules, the complete set of rules does not have to communicated up front, and when push comes to shove, anything goes as long as it's clear to another mathematician.

But at a deeper level, they deal with formalisms and manipulate information in a formal way. If you want to call that information manipulation language, I think that's reasonable because it can be used (and agreed upon) in an exchange of ideas.

For example, do you want to say the Fibonacci sequence starts "0 1 1" or "1 1"? It's just a definition thing, but if you and I agree on one or the other and then start talking about the Nth element of "the Fibonacci sequence", we are communicating with each other in terms of that. (And it's formal because we are basing things on not deviating from that.)

>when push comes to shove, anything goes as long as it's clear to another mathematician.

Well, yes! That's not inherent to Mathematicians. That's how all human communication works. That's what we use "natural" languages for.

What we use formal languages for is to minimise the ambiguity, imprecision and non-determinism (entropy) in natural languages.

Perhaps one way to put it: the purpose of natural languages is communication and context-setting. The purpose of formal languages is precision.

That line gets blurred in computer science (and in my own mind) because of Homoiconicity.

>For example, do you want to say the Fibonacci sequence starts "0 1 1" or "1 1"? It's just a definition thing

I don't want to say absolutely anything about Fibonacci in a vacuum.

The problem I am solving WITH Fibonacci will dictate whether it needs to start at "0 1 1", "1 1", or whether the the difference is immaterial.

Off-by-1 errors are just a fact of programmer's life. We make those decisions on case-by-case basis.

> if you and I agree on one or the other and then start talking about the Nth element of "the Fibonacci sequence", we are communicating with each other in terms of that.

What you are pointing out is problems of convention and consensus.

Off the top of my head I can think of a handful of strategies for coming to agree on the 0th value of the Fibonacci function in English. I bet you do too - all those things are intuitive to humans and we take them for granted.

In computer science many of those problems have already been formalised, and some have been solved.

https://en.wikipedia.org/wiki/Consensus_(computer_science)

P.S You have been using the concepts of "communication" and "information". Shannon formalised those!

P.P.S Fibonacci is an numerical formalisation of the Golden spiral.

In a nutshell, what I am pointing out is succinctly expressed by Donald Knuth.

Science is what we understand well enough to explain to a computer. Art is everything else we do.

The Chomsky hierarchy covers all of that.

It's linguistics for formal languages. Grammar, syntax and semantics together with reflection allows for formalisms and meta-formalisms.

It all culminates in Turing Completeness. Chomsky Type 0 grammars.

If you find something more powerful than a Chomsky Type 0 grammar - you have made a ground-breaking scientific discovery.

I'd say what mathematicians do is "think". We call the sort of thinking mathematicians do "mathematics". I get through quite a bit of grad stats in any given week and I'd say that what I'm not doing reading the computations of other mathematicians. I'm reading words in english, which try to explain concepts which are then sketched formulaically. I'm also reading proofs that are usually completed by a "mathematical" intuition and are very rarely if ever constructivist.

Maybe, that's just me busy thinking whilst the rest are busy computing :-)

By the way - this is rather circular and it begs questions.

> We call the sort of thinking mathematicians do "mathematics"

What kind of thinking do mathematicians do? Is it any different to the kind of thinking computer scientists do?

Once you are done thinking your thought() function returns a result in the form of language, no?

Or does thought() fail to halt?

Mathematics hasn’t been “computation” since the days of hand-tabulated lists of logarithms.

A lookup table is a particular case of a space-time trade-off.

https://en.wikipedia.org/wiki/Space%E2%80%93time_tradeoff

Sure, if you restrict yourself to intuitionistic logic... which is odd (to use the most charitable description I can give of it).

I need to go home and eat a bunch of weed edibles so I can read this comment.

Update: So I got drunk instead (which has basically the same effect on me).

Programming is math, except in the real world you have to deal with countless technical and business constraints. So unsurprisingly, theory != practice. The substance might just change in practice because a theoretical answer is completely impractical.

A formal language? Mathematics is a language of hand-waving. And I say that as a person who _loves_ math, even though I didn't take math beyond calc in college. When you translate math into algorithms and real programs, you begin running into problems that shape your solution. Really, you could come up with infinite different solutions to the same problem, all with different characteristics, use cases, strengths and weaknesses. There's no point in making a shared library, because it would be too fucking big and confusing. Better to formulate a solution yourself at this point, if you know what you're looking for, and tune it as you go.

I expect little to no cross-pollination because mathematicians love math and love their own work and love not having to deal with implementation issues, and have no desire to learn anything you mentioned. Unit testing, refactoring, ...none of it. Even many CS profs don't care, it's just the way it is -- a love of powerful ideas, not so much the dirty work of making them a reality. They theorize, and write off everything else as "applications." Nobody wants to write a beautiful algorithm, that also has to handle the sizes of different data types, and consider that not all the data may be in memory, and so on.

Reply on news.ycombinator.com