An Anecdote Against Slop Artifacts

The author describes their experience working on a paper about verifying exact samplers for continuous distributions using program logic techniques in the Iris framework. They mention the core trick of the project being simple and elegant, which Joe developed over a single weekend. The author's main contribution was exploring the potential of this trick and scaling it to verified implementations of complex sampling algorithms.

During the process, the author spent several months working on the idea, going through periods of intense mental strain. They verified the existence and convergence of ten thousand different Riemann integrals in Rocq, overcoming limited support for this in their analysis libraries. They also worked without the aid of AI, relying on organic mental effort to understand the code deeply.

A key aspect of the paper was stating an adequacy theorem, which required that a certain program, IsLessThanDyadic, would terminate with probability 1 when comparing real numbers to dyadic rational numbers. The program worked by iteratively comparing approximations of a real number against increasingly precise approximations of a dyadic number. The author explains how this process is justified for random sampling from nice probability distributions, like the Gaussian, where equality is almost never achieved.

The paper was accepted, but during the rebuttal process, the author realized that there was a sign error in the implementation of IsLessThanDyadic. Due to this error, the program was actually checking against increasingly coarser approximations, rather than the intended increasingly precise ones. This made the program nonterminating, making it unprovable and causing the proof checker to accept it without issue.

The author explains how the Loeb induction principle used for verification assumed the termination of the program, so a vacuous proof did not look significantly different from a correct one. The only difference was that a vacuous proof could be used to prove anything, including false statements about termination. In this case, the author was able to correct the sign error and ultimately finish the proof, ensuring the termination statement was true.