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

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?