Абмеркаванне

This is the most clear statement of Steele and White criteria I've seen.

Including their own paper that has somewhat inconsistent prose =)

@vitaut
The syntax makes the mathematicians in me very happy :) Excuse my ignorance, but what is this written in?

@jbowen This is Lean: https://lean-lang.org/. I absolutely love it.

@vitaut Is this a whole proof, or only the new functions you need for your proof?

@jgrg I have a proof of Roundtrips and Shortest for yy and it's ~2 kLOC o_O
https://github.com/vitaut/zmij/blob/main/test/verify.lean

@vitaut Right, so these are three conditions of correctness which you want to prove your algorithms satisfy? And you've done it for yy for two of them, but not zmij?

@jgrg Exactly. I picked yy because it is simple and it is used in zmij, just not for double. It should be straightforward to adapt the proof to another algorithm of a similar kind.