> 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

> 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 even after you trust the program, you then still have have to run the program to make sure the paper's result is correct. Far better to run the program once and then produce something you can check quickly than to require every peer reviewer to buy hundreds/thousands of dollars of compute time. Think P vs. NP: why force the reviewer to solve an NP problem when you can just as easily hand them a P problem. > Proofs can have "bugs", too But the reviewer's bug checking obligation is typically isolated to the paper at hand; i.e., the reviewer doesn't have to worry about the correctness of cited papers -- it's assumed those results are correct. By contrast, software implementations -- even for purely mathematical code -- often contain tens of thousands of lines of implicitly trusted code [1]. Reviewers therefore (rightly!) say of ad hoc programs submitted as a portion of a proof: "sorry, I can't possibly know whether there are any important bugs in these tens of thousands of lines of code upon when you depend". As a result, the SAT and theorem proving communities have developed highly trustworthy proof checkers so that the portion of code the reviewer has to trust can be meaningfully peer reviewed (and, more-over, peer reviewed apart from any particular theorem). [1] This is true even if you don't include things like the underlying operating system. Standard libraries, mathematics packages, compiler implementations, solver implementations, specialized software packages for the application domain, etc. etc. Some of this software a reasonable person will trust, but some of it really isn't interrogated well enough for the purpose of mathematical proof... and even just sorting out what's trustworthy and what's not can take a significant amount of time.