Feature wish: have the forward ASSN rule too

[Matafou]

This is a suggestion/feature wish. I always found the forward assignment rule much more pedagogical:

where x₀ must be a fresh (logic) variable.

I can't estimate the amount of work for dealing with fresh variables safely (especially when gluing proofs?), but it would greatly help students imho.

Congrats with this tool. It is very nice!

[joom]

Implementing it with a quantifier like Floyd (⊢ {P} V := E {∃v. V = E[v/V] ∧ P [v/V]}) can make it easier. I can easily add that. Would that work for you?

Also, just out of curiosity, are you using this in a course? I'd love to know where and what the course looks like overall.

[Matafou]

It would probably be ok, but the pre-post will become more complex and we will need more conseq rules to simplify them.
I agree that the fresh checking is annoying though. Because it is not modular. I would give it a try anyways.

I used it in a very short introduction course on Hoare logic, yes. And it was quite nice. Thanks again!