> Dijkstra's Guarded Command Language is a specification language, sort of, but it's better looked at as a very simple programming language for use with Floyd/Hoare/Dijkstra's axiomatic semantics. (Which didn't get mentioned at all. Sniff.)
This struck me too. There is an ur-language there, but it's not GCL rather it's Hoare triples and subsequently predicate transformer semantics and Boolean structures, as defined by Dijkstra and Scholten (among others, but they're the ones best known to me). So in that sense the ur-language for program specification is something we might call "mathematical logic." And predicate transformer semantics, when you get right down to it, is leaning on Leibniz's principle about as hard as biology leans on H-bonds. As you say, GCL is just a simple language that has a well defined predicate transformer semantic and an interesting approach to nondeterminism that is suitable for the kind of research Dijkstra was doing. One could theoretically define predicate transformer semantics for any language, although it would be a prohibitively difficult challenge for most if not all languages in common use today. Whether that's a problem with predicate transformer semantics or the languages we have is a matter of opinion I suppose.
Also predicate transformer semantics were extended to support concurrency by Lamport[1].
I'm still hoping for the day when assertional arguments fully banish behavioral ones, but it looks like it's still a long way off.
For some reason, I ended up calling those "axiomatic semantics"; predicate transformer semantics is a much better name.
One of the weaknesses of PTS for common languages is that statements and expressions have very complicated semantics, compared to the relatively simple semantics of GCL and other simple treatments. One of the nice things about Frama-C (and I think the GNAT SPARK tools) is that, when you are using the WP (Weakest Precondition) module to prove properties of C code, it can automatically generate assertions that describe overflow/underflow, which then forces you to put the appropriate preconditions on function parameters. :-)
By the way, have you run across K. Rustan M. Leino's recent book, Program Proofs, and the Dafny language. It's the most recent and so far, best book I've seen on the style and technology.
I was doing some work on defining PTS for a subset of Go, so I'm definitely aware of how tricky it can get. While handling early return requires some care, the existence of goto and break in particular caused me considerable trouble defining semantics for the loop construct. Needless to say that's barely scratching the surface, and Go is a pretty small and intentionally simple language as far as popular ones go.
If I were to try again, I think I'd look at building GCL as as simple Lisp and then build higher level constructs as macros that would inherit their semantics from the well-defined GCL's composition rules. Then of course if I wanted to succeed in the marketplace I'd throw that out, rewrite the Lisp part as an AST library, probably in Rust or Go, and then lex and parse it from some squiggly brace syntax. That syntax in turn would probably be a subset of the grammar of some popular language to ease practical use. At then point it could get grafted on as a kind of linter maybe.
I'm also particularly excited about the prospect of deducing appropriate preconditions from stated postconditions/assertions. The very concept of working backward from the desired end to the known beginning is so elegant and intuitive that millions of school children independently discovered it when solving mazes.
I am somewhat familiar with Dafny. It looks really neat and I've written some toy code. I'm not familiar with that book though, so I'll have to add it to my reading list.
This struck me too. There is an ur-language there, but it's not GCL rather it's Hoare triples and subsequently predicate transformer semantics and Boolean structures, as defined by Dijkstra and Scholten (among others, but they're the ones best known to me). So in that sense the ur-language for program specification is something we might call "mathematical logic." And predicate transformer semantics, when you get right down to it, is leaning on Leibniz's principle about as hard as biology leans on H-bonds. As you say, GCL is just a simple language that has a well defined predicate transformer semantic and an interesting approach to nondeterminism that is suitable for the kind of research Dijkstra was doing. One could theoretically define predicate transformer semantics for any language, although it would be a prohibitively difficult challenge for most if not all languages in common use today. Whether that's a problem with predicate transformer semantics or the languages we have is a matter of opinion I suppose.
Also predicate transformer semantics were extended to support concurrency by Lamport[1].
I'm still hoping for the day when assertional arguments fully banish behavioral ones, but it looks like it's still a long way off.
[1] https://lamport.azurewebsites.net/pubs/lamport-win.pdf