4 ms·

This is great! Thanks for sharing your approach. I come at it from the perspective of a working programmer who wants to improve his craft. Mostly I just think

by User23 2y ago

This is great! Thanks for sharing your approach. I come at it from the perspective of a working programmer who wants to improve his craft. Mostly I just think through the (pseudo) formalism because frankly most commercial code isn’t terribly complex when properly designed (or it’s such a mess time constraints don’t permit working through it formally). From time to time I work through the proofs though, especially in hard to test code. Also, I’ve been fortunate enough that in my career I’ve done some actual language semantics work in the mechanical checking space. From that perspective, I kind of like “;” for composition, virtually entirely because it effectively works as a statement separator. E.g.: if Pred(x) DoThing(x); DoOtherThing(x) end At a glance it looks like a statement terminator with a special elision rule for the end of a block, but really the body is just a single compound statement with semantics that can be determined from its constituent predicate transformers. I fully recognize how that’s hardly a compelling reason logically, but sometimes things just appeal aesthetically. Also I guess it might simplify an implementation to be able to assume that every apparent “block” is actually a single, possibly compound, statement. There might be some interesting parsing implications too. I’m practically ignorant of concatenative languages (Lisp is my hammer of choice for playing around with language ideas). Perhaps I should fix that by hacking up a toy Forth inspired by Dafny.

kragen 2y ago
you're welcome! i'm glad you enjoyed it i agree that ';' as a statement separator is analogous to relational composition for predicate transformer semantics (which is plausibly why dijkstra chose it) incidentally ';' in ocaml works syntactically in the way you want; it's a two-argument version of lisp progn the block semantics i find most appealing is the semantics of henry baker's comfy-65/comfy-80, in which each statement has one entry point, which i'll call go, and two (possibly unused) exits, a yes exit and a no exit. (baker's nomenclature differs!) regular computational statements like assignments only use their yes exit, but comparisons transfer control to one or the other depending on whether the comparison succeeds or fails. to build a whole subroutine out of such atomic statements you have four combining operators. baker gives them lisp function names, but we could use infix operators for them instead, and describe how they wire things up with equality constraints: (a ; b) : go = a.go, a.yes = b.go, yes = b.yes, no = a.no = b.no (a ∨ b) : go = a.go, a.no = b.go, no = b.no, yes = a.yes = b.yes (¬a) : go = a.go, no = a.yes, yes = a.no (while a b) : go = a.go, a.yes = b.go, b.yes = go, a.no = yes, b.no = no (hopefully that notation i just made up is clear, but let me know if not) baker has a couple of other combining constructs, but they're not fundamental. actually even ∨ is superfluous; (a ∨ b) ≡ ¬(¬a ; ¬b), so statement sequencing is the same thing as logical conjunction. you can add a do-while operator for loops with the loop test at the bottom which is dual to while in the same way baker implements his compiler as a lisp function (compile statement yes no) which takes memory addresses where yes and no should transfer control, and returns an entry point (go); for the combining forms it recursively invokes itself, so it ends up generating code backward starting from the top of memory. his implementation of while requires inserting an unconditional jump at the end of the loop which is later backpatched to jump to the beginning of the loop comfy has in common with forth that boolean expressions and blocks of statements aren't non-overlapping magisteria, the way they are in the more mainstream formulations; in forth, both a block of statements like s" x = " type x ? cr and a boolean expression like x @ y @ > are just doing one damn thing after another. but forth handles its booleans in the same way as lisp, c, or pascal, pushing a comparison result on the stack which is consumed by a following conditional-branch word, an approach which in forth results in inefficient and unsafe code for boolean operators because it can't short-circuit them like c's && and || while this is very appealing aesthetically, i can't help but feel that it might make proofs of correctness unnecessarily difficult. you can make some statements about control flow dominance: in any of a ; b, a ∨ b, or while a b, you know that b never runs unless a ran previously. but when you get out of a construct, how do you know what ran inside the construct? in a long sequence like a ; b ; c ; d any of the items in the sequence can potentially leap out with a no, skipping the later items maybe you could consider comfy statements to be pairs of predicate transformers, one for the yes exit and one for the no exit?

by User23 2y ago

kragen 2y ago

you're welcome! i'm glad you enjoyed it i agree that ';' as a statement separator is analogous to relational composition for predicate transformer semantics (which is plausibly why dijkstra chose it) incidentally ';' in ocaml works syntactically in the way you want; it's a two-argument version of lisp progn the block semantics i find most appealing is the semantics of henry baker's comfy-65/comfy-80, in which each statement has one entry point, which i'll call go, and two (possibly unused) exits, a yes exit and a no exit. (baker's nomenclature differs!) regular computational statements like assignments only use their yes exit, but comparisons transfer control to one or the other depending on whether the comparison succeeds or fails. to build a whole subroutine out of such atomic statements you have four combining operators. baker gives them lisp function names, but we could use infix operators for them instead, and describe how they wire things up with equality constraints: (a ; b) : go = a.go, a.yes = b.go, yes = b.yes, no = a.no = b.no (a ∨ b) : go = a.go, a.no = b.go, no = b.no, yes = a.yes = b.yes (¬a) : go = a.go, no = a.yes, yes = a.no (while a b) : go = a.go, a.yes = b.go, b.yes = go, a.no = yes, b.no = no (hopefully that notation i just made up is clear, but let me know if not) baker has a couple of other combining constructs, but they're not fundamental. actually even ∨ is superfluous; (a ∨ b) ≡ ¬(¬a ; ¬b), so statement sequencing is the same thing as logical conjunction. you can add a do-while operator for loops with the loop test at the bottom which is dual to while in the same way baker implements his compiler as a lisp function (compile statement yes no) which takes memory addresses where yes and no should transfer control, and returns an entry point (go); for the combining forms it recursively invokes itself, so it ends up generating code backward starting from the top of memory. his implementation of while requires inserting an unconditional jump at the end of the loop which is later backpatched to jump to the beginning of the loop comfy has in common with forth that boolean expressions and blocks of statements aren't non-overlapping magisteria, the way they are in the more mainstream formulations; in forth, both a block of statements like s" x = " type x ? cr and a boolean expression like x @ y @ > are just doing one damn thing after another. but forth handles its booleans in the same way as lisp, c, or pascal, pushing a comparison result on the stack which is consumed by a following conditional-branch word, an approach which in forth results in inefficient and unsafe code for boolean operators because it can't short-circuit them like c's && and || while this is very appealing aesthetically, i can't help but feel that it might make proofs of correctness unnecessarily difficult. you can make some statements about control flow dominance: in any of a ; b, a ∨ b, or while a b, you know that b never runs unless a ran previously. but when you get out of a construct, how do you know what ran inside the construct? in a long sequence like a ; b ; c ; d any of the items in the sequence can potentially leap out with a no, skipping the later items maybe you could consider comfy statements to be pairs of predicate transformers, one for the yes exit and one for the no exit?