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.
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.