Ask HN: Is writing a math proof like programming without ever running your code?
And if so, wouldn't most math proofs be full of errors just like untested code?
All the important distributed algorithms were formally verified using proof assistants. The entire field of "formal verification" is nothing but writing proofs to verify correctness of software & hardware. There are tons of lectures on formal verification.
Interesting is subjective.
Your conclusion doesn't follow from the premises.
I assert that a useful program is more interesting than a useless one.
If it's useful (and interesting) as a program, and uninteresting as a proof, then there is a difference between proofs and programs, not at the level of the Curry-Howard Correspondence, but at the level of human life. As a program it can make your life easier; as a proof it's not going to change anyone's life in any way whatsoever.
1. There are non-constructive proofs, ie proofs that show that something exists, but do not provide an example (but rather derive a contradiction from the assumption that it doesn't exist, for example). Those are not really akin to running code. The Banach-Tarski paradox is a particularly striking example: You can decompose a ball into 5 pieces and reassemble them into 2 balls of the same size of the original.
https://en.wikipedia.org/wiki/Constructive_proof
https://en.wikipedia.org/wiki/Banach–Tarski_paradox
2. Don Knuth famously sent a colleague some code with the warning "Beware of bugs in the above code; I have only proved it correct, not tried it."
…if you accept the law of excluded middle.
https://inspirehep.net/files/20b84db59eace6a7f90fc38516f530e...
using a wavepacket basis parameterized in phase space. I wrote extensive unit tests to confirm everything, I even know I got the signs right.
Errors are really common in “mathematical physics” papers, some of the papers that inspired that work had errors in the middle of long calculations that got past the peer reviewers and probably everybody who didn’t try to reproduce the results.
Although the calculation was correct, the result wasn’t as useful as we’d hoped because we had no idea how to calculate the Maslov index because a periodic orbit in classical mechanics is no longer a periodic orbit when you consider the change in the shape of the wavepacket and with no periodic orbit there is no topological invariant. My thesis advisor and another student were able to reuse the math for something where they didn’t need the Maslov index so it wasn’t a complete loss.
When you tell a mathematician "this function takes an integer" or "that function always returns a string" they will immediately jump to looking for counterexamples to see if they can break it. They do this because they know that one counterexample breaks a proof. Programmers who think that way tend to produce fewer bugs imo.
I suspect that people with higher IQ can probably write code with fewer errors when no testing is done.
I don't think that's it. As a rule, the tests we write for code don't prove anything in the mathematical sense. They are more along the lines of "OK it didn't break with an input of 6 or 7, now let's try 8". IOW we treat the code like a black box and see how it responds to various inputs.
Mathematical proof is a different kind of intellectual activity. It's about showing that one fact is a logical consequence of another. You don't test a proof because the proof is the outcome of testing. But that testing is almost always as general as possible. In code, you might test that a given function works with the numbers 1-100 by trying 1 and 100 and simply assuming that it'll behave the same way for the numbers in the middle. This is often adequate, and it's probably the best you can do anyway, but it's not a proof (except for those specific inputs).
A mathematician would instead analyze the implementation of the function to show that it's logically guaranteed to work for 1 <= x <= 100. But then the proof would only exist in their head, or on paper, in human readable form. Can you write automated tests that analyze code in that way? Maybe but that's beyond me.
Testing can be combined with inductive reasoning to validate code. Say we have some recursive function with 7 base cases, and a recursive case. We can use testing to validate the 7 base cases, and then an inductive argument that the recursive case is correct.
Personally I think we (software developers) should do more of that - i.e. take implementation details into account when designing tests, instead of treating components as black boxes, and when we change those implementation details, examine the tests to see what assumptions were made that now need to change. It's harder but it's closer to really proving something general about the code.
Like say you develop a function by adding cases, TDD style. Then you see there is a generality there and refactor so the individual cases go away. The tests probing those cases still have validity, but no value.
If my understanding is correct, it can't "prove" any properties, only disprove them.
For concretely proving properties of a program, you would need something like Idris's dependent type system, where you can prove that a function always returns a sorted list, for example.
https://github.com/nick8325/quickcheck https://www.idris-lang.org/
Almost. If your generators exhaust the input space then the property is proved.
Your ability to catch errors tends to be closely linked to the amount of time you've spent working in a particular area - because you build up a mental suite of test cases to check every claim against. One mistake I see occasionally is jumping into a brand new area of math and moving just as quickly as you would in the old area where you had more expertise, making huge blunders every step of the way. When you enter a new area, you have to go really excruciatingly slowly as you build up the intuition and suite of examples.
Almost every math paper contains an error or two - they are usually easy for an expert to fix (the equivalent of leaving out a semicolon at the end of a line in C++, takes only a moment to fix if you have familiarity with the language - but incredibly frustrating to a user who doesn't know how to make the easy fix).
Tests in programming are more akin to double entry book-keeping in accounting: you specify the same program twice (not really, you usually have manually precalculated a few cases, but that's roughly the point).
As such, mathematical claims (theorems, lemmas or anything, really) requiring proofs are "integration tested" in applying them elsewhere (basically, they give reasonable results). This implicitely tests their proofs too.
For sure, there are probably a lot of fringe theorems based on invalid proofs.
That is the reason more people find programming enjoyable but struggle with mathematical proof writing.