11–20 of 32 posts
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.
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 things such as side effects and complexity — its not trivial stuff!
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…
What you probably mean is something like nice abstract accounts of memory models for C that at the same time capture all the optimisations modern C-compilers want to do, while still being implementable on existing CPUs. That is indeed an open problem [1].
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…
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 progspecs, but defining that progspecs are pairs of (relation, set).
> 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.
Mathematicians think programming is mathematics. Programmers think they're simulating the mind of a mathematician!
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…
What you probably mean is something like nice abstract accounts of memory models for C that at the same time capture all the optimisations modern C-compilers want to do, while still being implementable on existing CPUs. That is indeed an open problem [1]. True. Although CompCert [1] is a nice effort toward that goal: a proved C compiler that covers almost all C99 with many optimizations implemented and proved sound.…
The problem with memory models is not so much verifying it in a mechanised way, but inventing something suitable at all.
Anyone 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?
Another oddity: "Object oriented" programs are defined as functions {0,...,n} -> O where O is "a set of objects". Yet: A program is defined to be an endo-relation SS. Accordingly, we have O = {0,...,n}.
I don't see how this definition gives any insight on the nature of object oriented programming.
Now for the strangest thing: The definitions of "object oriented" and "procedural" involve differentiating between possible condidates for S. Yet the only property a set without any context really has is its cardinality.
So we can rephrase the definitions of "object oriented" as follows:
An "object oriented" program is a set S together with a total function S -> S with S finite. ([total function] AND [S finite])
Negating, we arrive at the definition of "procedural program":
A "procedural" program is either a relation S S that is not a total function (no restrictions on the cardinality of S) OR any relation SS but S must be infinite. ([not a total function] OR [not S finite])
I don't see how this definition captures the notions of object oriented programming and procedural programming in any meaningful way.
But maybe the author will appear here and to clarify his ideas.
Earlier quoted context omitted.
What you probably mean is something like nice abstract accounts of memory models for C that at the same time capture all the optimisations modern C-compilers want to do, while still being implementable on existing CPUs. That is indeed an open problem [1]. True. Although CompCert [1] is a nice effort toward that goal: a proved C compiler that covers almost all C99 with many optimizations implemented and proved sound.…
CompCert uses tame optimisations, and compiles to mainstream architectures nothing exotic. Most of all, CompCert does not deal with concurrency as far as I'm aware. Concurrency is where memory models matter. The problem with memory models is not so much verifying it in a mechanised way, but inventing something suitable at all.
The problem with memory models is not some much verifying it in a mechanised way, but inventing something suitable at all.
I'm aware of some work done a few years ago by people working on weak memory models and extending CompCert with some concurrency primitives: http://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/
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…
See for example [ http://chu.stanford.edu/guide.html ]
Earlier 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.