Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

New Paper: Theory of Programs

bertrandmeyer.com

Post reply on HN
Print view View original

21–30 of 32 posts

Re: New Paper: Theory of Programs

#21

Post by buttproblem »

mafribe wrote: post #10
buttproblem wrote: post #5

At least since 1935 [1, 2] people have been trying to formalize all of mathematics with set theory. I always thought this was fairly interesting, similar to how the real numbers can be modeled in a language using dependent types like Coq. However, I always found Hoare logic, and its concurrent extension Rely--Guarantee from Jones, to be quite easy to understand. The more interesting part is how to do this automatical…

At least since 1935 people have been trying to formalize all of mathematics with set theory. Cantor invented set theory for this purpose in the 1870s. By 1935, Goedel's incompleteness theorems had shown the limitations of this (and any other) foundation of mathematics. Hoare logic is not a foundation of maths, but an approach towards specification and verification of programs. As such it is in the same space as Curry…

Thanks for the interesting history on set theory. However, if you read [1] or the first chapter of [2] in my reply you'll see that the strides to formalize mathematics started in 1935 so something does not add up.

I did not intend to say Hoare logic being a foundation of mathematics, this was unclear in my post since I just abruptly changed topics. However, i would be delighted to read someone attempting to do just that.

What I intended to say is that the posted paper is basically a formulation of Hoare logic using set theory.

By this I meant both specifying program semantics and proving program properties. As in, the automated construction of Hoare pre/post annotations or for concurrency rely--guarantee annotations. To me, this is bringing languages without depends types closer to similar kinds of correctness guarantees.

Thanks for the clarifications on semantics. You hit the nail on the head.

Re: New Paper: Theory of Programs

#22

Post by black_knight »

ble wrote: post #14
black_knight wrote: post #12

Just skimming the definitions they seem more than a bit naïve. A relation is really a more general thing than a program, since it need not be computable in any way. The real mathematical models of programming are not all that difficult to understand. The most famous, the Turing machine, is really just a finite set of states and a function on it. The complications which arise later are real complications, describing t…

Meyer is trying to move up one level of abstraction; the `programs` he is talking about are synonymous with `specifications` so right away those words are being used in an atypical fashion. Calling them `progspecs` would be gross and newspeak-y and calling them `program specifications` would be verbose. Regardless, the theory of these `programs` may indeed be useful. Also, he's not saying that all relations are progs…

Mathematical definitions are expected to be complete, in that if I define an A to be a pair of a B and a C, with no further restrictions, I will accept any such pair as an A.

As an example of a more abstract way of looking at programming, take a look at domain theory. A domain is a set with a relation on it. But opposed to the current topic, there are more restrictions making a beautiful theory, capturing things such as lazy evaluation.

Re: New Paper: Theory of Programs

#23

Post by black_knight »

groar wrote: post #9
mafribe wrote: post #8

Earlier quoted context omitted.

By Curry-Howard, the program is the proof, albeit usually not of an interesting proposition.

In a rich type system, a program is the proof of its own specification. Which is usually as interesting as the program itself.

«Which is usually as interesting as the program itself.» And ten times as hard to write. Not just saying that — I spend most of my time in Agda, and even simple things are rather difficult. But I think this will improve as we learn the right way to look at things.

Re: New Paper: Theory of Programs

#24

Post by tel »

buttproblem wrote: post #21
mafribe wrote: post #10

Earlier quoted context omitted.

At least since 1935 people have been trying to formalize all of mathematics with set theory. Cantor invented set theory for this purpose in the 1870s. By 1935, Goedel's incompleteness theorems had shown the limitations of this (and any other) foundation of mathematics. Hoare logic is not a foundation of maths, but an approach towards specification and verification of programs. As such it is in the same space as Curry…

Thanks for the interesting history on set theory. However, if you read [1] or the first chapter of [2] in my reply you'll see that the strides to formalize mathematics started in 1935 so something does not add up. I did not intend to say Hoare logic being a foundation of mathematics, this was unclear in my post since I just abruptly changed topics. However, i would be delighted to read someone attempting to do just t…

I went ahead and skimmed the first chapter of [2] (again; I own it) and don't see it justifying that this stuff began in 1935. Indeed, it suggests, e.g., that a major difficulty of the program to formalize all of math in set theory, Russell's Paradox, was discovered in 1901 and then immediately notes that set theory itself was begun by Cantor decades before.

It also then mentions how Set Theory was formalized and fixed through the introduction of formal classes (which fixed the size concerns discovered by Russell by outlawing them---and actually Russell himself proposed a system which did exactly this, his "rammified hierarchy" almost immediately after discovering his paradox; it is the foundational model of the Principia Mathematica which was published in three volumes in 1910, 1912, and 1913) and that these were in use by the mid 1920s.

In fact, the first mention of dates in the 1930s occur in Hilbert's finitist attempts to prove consistency and Godel's destruction of that program.

What you're probably referring to is Bourbaki's work. This wasn't an initial attempt by any means but instead a broad reaching program to popularize the methods of sets that had been previously established. This was the moment of catastrophic phase change when all old mathematical concepts were suddenly shown to be suspect if they could not be axiomatized set theoretically—so certainly when a bulk of work occurred.

But all said, it is certainly the case that set-theoretic foundations of mathematics was a 1870-1930 affair.

Re: New Paper: Theory of Programs

#25

Post by tel »

im3w1l wrote: post #20
mafribe wrote: post #8

Earlier quoted context omitted.

By Curry-Howard, the program is the proof, albeit usually not of an interesting proposition.

Bottom is a member of every type, so all Haskell programs correspond to proofs of trivial propositions. Or that is my understanding anyway. And something similar should be true for common imperative languages.

Not quite. Bottom as a member of every type means that you cannot trust my proof (x : A) without examining it and that your examination may be non-terminating. That said, it you examine a realizer and terminate then you have a genuine proof of a potentially non-trivial theorem.

The reason why most Haskell theorems are trivial is because lacking dependent types means that we cannot ask for interesting theorems. `3 :: Int` is a perfectly nice proof that "Integers exist" which is a little silly.

Re: New Paper: Theory of Programs

#26

Post by nmrm2 »

What I couldn't find was an answer to the question "why?"

I could see this being an interesting basis for teaching Computer Science in high schools, where a text like this functions in a way similar to Euclid in high school Geometry courses. I'm pretty sure there aren't any non-exceptional examples of high school Computer Science courses (e.g., the AP CS course is better described as an Intro to Computer Programming course).

And in any case this is a nice exposition.

But aside from that, I'm not sure I see any new insights here about CS/verification, nor any suggestions for research directions that aren't already extensively explored. Perhaps I'm missing something, though.

(Edit: There's a list of suggested future work at the end of the paper. I guess I get it now; although all of these things have been done in verification/PL -- and even by non-type-theorists -- they almost always involve the development of a new logic, and aren't done in pure set theory. So certainly there's a lot of work to do if you want to do things in this style. But I'm still trying to see the benefit of this style, aside from pedagogic or philosophical benefits. Is my inexperience in this area blinding me from some obvious potential? I don't know much about non-high-school set theory.)

Re: New Paper: Theory of Programs

#27

Post by AnimalMuppet »

nmrm2 wrote: post #26

What I couldn't find was an answer to the question "why?" I could see this being an interesting basis for teaching Computer Science in high schools, where a text like this functions in a way similar to Euclid in high school Geometry courses. I'm pretty sure there aren't any non-exceptional examples of high school Computer Science courses (e.g., the AP CS course is better described as an Intro to Computer Programming…

Building a unified framework for all of programming theory is useful, even if it provides no new insights. It provides a clearer basis for thinking about what we already know, and thereby makes the new insights easier. So even if the new insights aren't here yet, it makes it more likely that they eventually come.

Re: New Paper: Theory of Programs

#28

Post by nmrm2 »

AnimalMuppet wrote: post #27
nmrm2 wrote: post #26

What I couldn't find was an answer to the question "why?" I could see this being an interesting basis for teaching Computer Science in high schools, where a text like this functions in a way similar to Euclid in high school Geometry courses. I'm pretty sure there aren't any non-exceptional examples of high school Computer Science courses (e.g., the AP CS course is better described as an Intro to Computer Programming…

Building a unified framework for all of programming theory is useful, even if it provides no new insights. It provides a clearer basis for thinking about what we already know, and thereby makes the new insights easier. So even if the new insights aren't here yet, it makes it more likely that they eventually come.

I guess my question is, why set theory, as opposed to building [new] logics on top of other semantic models (e.g. operational semantics or reachability relations)?

(I don't doubt there are compelling reasons, I just don't know enough about set theory or programming theory to know what they are. Other than the clear benefit of this approach over others in "elementary" educational settings, e.g. US high schools)

Re: New Paper: Theory of Programs

#29

Post by AnimalMuppet »

nmrm2 wrote: post #28
AnimalMuppet wrote: post #27

Earlier quoted context omitted.

Building a unified framework for all of programming theory is useful, even if it provides no new insights. It provides a clearer basis for thinking about what we already know, and thereby makes the new insights easier. So even if the new insights aren't here yet, it makes it more likely that they eventually come.

I guess my question is, why set theory, as opposed to building [new] logics on top of other semantic models (e.g. operational semantics or reachability relations)? (I don't doubt there are compelling reasons, I just don't know enough about set theory or programming theory to know what they are. Other than the clear benefit of this approach over others in "elementary" educational settings, e.g. US high schools)

Lowest total cognitive load?

That is: If I build my theory on a complicated foundation, then you have to learn the complicated foundation before you can even start to learn my theory.

On the other hand, if I build it on a simple foundation, but that simple foundation means that the theory itself has to jump through a bunch of hoops because the foundation is too simple, that can also make the total (foundation + theory) harder to learn and understand.

So the sweet spot is to use the simplest foundation that does not unduly complicate the theory. (And that may change, depending on target audience.)

Is set theory the best answer? I have no idea, but all of programming in 28 pages, built on a foundation only of set theory, is very impressive.

Re: New Paper: Theory of Programs

#30

Post by Retra »

amelius wrote: post #7
fizixer wrote: post #2

> Programming, wrote Dijkstra many years ago, is a branch of applied mathematics. This is as effective as saying "X is a branch of philosophy", where X is any discipline. It's probably true for every discipline, but what's the point? Also every X is a branch of physics, because we live in a physical universe and everything is inside it (so even pure mathematics is a branch of physics). And finally X is a branch of co…

Programming is like mathematics, except all proofs are omitted.

A program is a proof of the result (theorem) computed from the inputs (axioms) supplied.
Post reply on HN