The ergonomics of modern proof writing just get better and better.

This is just a proof about a C program. Nothing in the program is important from a philosophical standpoint. But the logic and implementation is swell.

The logic is called higher-order impredicative concurrent separation logic. The separation part allows me to only have to think about small parts of the C program at a time. Multiple people can work on the same proof without stepping on each other.

The implementation allows for a lot of automation in proof writing. Most of the heavy lifting and boring stuff, like interfacing integers to registers of 64 bits are done. There is plenty of room to create more automation for common proof strategies.