Back when I was working on proof of correctness, when that was a very new thing, I was using the Boyer-Moore theorem prover remotely on a large time-shared mainframe at SRI International. At the time, you needed a mainframe to run LISP. I was working on proofs of basic numeric functions for bounded arithmetic. So I was writing theorems with numbers such as 65536. This caused the mainframe to run out of memory, page o…
Can we have a moment for the folks who managed to turn numerical purity into integers being O(n)? It's unbearably beautiful... And I do mean unbearably...