nrfc

3 ms·

1. 1.▲
   by nrfc 10y ago

   > This is no different from a typical math paper It's substantially different from a typical math paper. First because programs are typically much larger than even large mathematical proofs (more on this below). Second, because ev
2. 2.▲
   by nrfc 10y ago

   The authors used this tool: https://www.cs.utexas.edu/~marijn/drat-trim/ There are publications and examples on the website that explain how the compression the authors used works.
3. 3.▲
   by nrfc 10y ago

   > If you verified the code performed the correct function, ensured it ran correctly and computed the result, then the code itself serves as most of the proof But then you have to trust their program doesn't have any bugs, and chec