Magos Logis Logan @jmw150@qoto.org

Well, fewer than 10 days till classes start. Time to reset all of the scripts.

Also staying home again, because I am a soft skinned baby. (And we computer whisperers will probably get more done without having to change out of pajamas and drive places, right?)

Stay safe everybody.

Enjoyable math is optimal in the intuinistic style of thought. Profound math is optimal in the Platonists style of thought.

It was love at first sight.

Even after close to a decade, I still kick random problems apart with it. That is some good shit.

Geometric algebra is pretty fun to be honest.

Well, birthday is coming up. Please slow down, time... 😅

I leave the house for 5 minutes and I hurt my back. Guess what I am doing for the rest of the day.

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.

So good. lol

https://en.wikipedia.org/wiki/Boolean_Pythagorean_triples_problem