Comment by IanCal

This is a nice reminder for people.

Cool project!

This is really interesting, I’ve been very interested in the power of checks for code and things like hypothesis (which seem very similar in terms of writing a “for this kind of case, this holds true”, obviously different in terms of statistical checking vs actual proof).

I’ll have to explore and this isn’t my field so this isn’t a substantive comment and this may be bikeshedding but I found the game example a little confusing at first because we’d want winning to be possible. It fits the context of stopping a bad thing happening if it’s “evil actor can’t do X” and if your mind is on CTF but games we want to win.

Potential changes:

Make it a proof that the game can be won.

Make it require something first - so the game can’t be won unless the key is found for example. End result is still roughly the same and the failure case is still the same (walk over side of game) but it’s the kind of thing I’d want encoded in a puzzle game - game is winnable, but not winnable without getting the key first.

Since my other direction normally would be quickcheck style, I’d be interested in cases that are statistically hard to find but easy to prove exist. And in fairness, the other way too I guess. When to use each approach.

In the spirit of your comment, these are not things I see as failings, they are not things I in any way expect to be changed or done, they are intended as just an outsiders perspective if useful.

Thanks for making things, and thanks for releasing them!