How would you use Hoare logic to verify an API migration did not introduce new behaviors? If the API spec allows multiple implementation choices, you need to reason about relational liveness over nondeterministic executions, but relational Hoare logics don't support this kind of reasoning... until now!

Check out my APLAS talk "RHLE: Modular Deductive Verification of Relational ∀∃ Properties" Monday at 1:30p.

🗣️​ Talk abstract:

📄​ Preprint:

Local Indiana Politics 

Always check the local paper for the one unhinged school board candidate who, when given ample time to compose a single paragraph, decides to go with something like this.

I have lived seeing my work appear "years after the shine has dulled," and I can say it is without question a more discouraging experience than the rejections themselves.

Going through some NYT crossword archives and absolutely nailing it.

At the beginning of this video, the two fencers touch each others' arms to test that the scoring machine is working. It isn't, but everyone is on autopilot and nobody notices. The fencers then fence a full touch, which gets annulled because the machine isn't working. This is a toot about CI.

Did you know the original proof assistants were nothing but swords, axes, and arrows? We've come a long way.

Having a real hard time reheating food in this microwaved-sized void for some reason.

Show thread

Also some of the attempts to match books from the import are pretty amazing. I'm sure these two books are basically the same thing.

Show thread

Kid has been into Sonic the Hedgehog lately (b/c new movie), so naturally we broke out the Genesis.

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.