New Paper: Theory of Programs
bertrandmeyer.com
New Paper: Theory of Programs
1–10 of 32 posts
Re: New Paper: Theory of Programs
#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 computer science because computation and information processing sometimes appears to be more fundamental than everything else. E.g., physics cannot answer the question, "are we living in a matrix-like simulation?" but if we really are, the whole physical universe is mere computation happening in some higher dimension.
I like to think of Mathematics, Computer science, Physics, and Philosophy to be deep and insightful realms of human thought, and they have many connections but also many unique attributes.
Re: New Paper: Theory of Programs
#3Anyone find the definition of `functional` a little bit odd?
Is there a reason why a "no-op" or identity function should be considered imperative? Or why a program must be imperative if at least one post-execution state is also a valid pre-execution state?
Re: New Paper: Theory of Programs
#4> 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…
If subject X is fundamentally about underlying subject Y, then reasoning using the tools of subject Y might help you to have powerful (fundamental) insights into subject X.
I take your point, nonetheless.
Re: New Paper: Theory of Programs
#5At 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 automatically for a user. Abstract interpretation is one way to do this, but this necessarily requires mapping some programming language to your mathematical model. However, determining the formal semantics of mature programming languages, even C, is still open research (e.g., see papers on Semantics in PLDI [3] 2015).
TLDR: verification is hard.
[1] https://en.wikipedia.org/wiki/Nicolas_Bourbaki
[2] Topoi, the categorial analysis of logic. Goldblatt, Robert. http://digital.library.cornell.edu/cgi/t/text/text-idx?c=mat...
[3] http://conf.researchr.org/track/pldi2015/pldi2015-papers#pro...
Re: New Paper: Theory of Programs
#6> 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…
I disagree and I think you are interpreting "applied mathematics", "physics", and "computer science" overly literally - rather than labels for fields of study.
The point in the article is that programming is no longer just Applied Mathematics, it's also very much a discipline of Engineering as well. Anyone who studies these fields should understand the difference.
You are right, that these terms can apply to deep realms of human thought - but I think they are less useful terms under that definition.
Re: New Paper: Theory of Programs
#7> 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.
Re: New Paper: Theory of Programs
#8> 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.
By Curry-Howard, the program is the proof, albeit usually not of an interesting proposition.
Re: New Paper: Theory of Programs
#9Earlier quoted context omitted.
Programming is like mathematics, except all proofs are 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.
Re: New Paper: Theory of Programs
#10At 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.
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-Howard based programming languages like Idris and Agda with dependent types. The main differences between the two are that (1) Hoare logic is not restricted to constructive reasoning and (2) Hoare logic is not integrated with the programming language, so programming and proving are distinct activities. Depending on your philosophical outlook, either (1) or (2) or both can be seen as major advantage or disadvantage.
how to do this automatically
determining the formal semantics ... is still open research
[1] https://www.cl.cam.ac.uk/~pes20/cpp/c_concurrency_challenges...