Even if I write a formal proof, I'm not guaranteed that my program won't index out of bounds. Formals proofs have errors in them all the time. I want dynamic checks to catch me in those cases.
Further to the point, let me reiterate: programmers do not (in almost all cases) write these proofs you are talking about.
> My reasoning skills exceed that of my compiler and I can thus determine that certain designs are type-safe that my compiler cannot.
Anyhow. Back to your last comment:
> Even if I write a formal proof, I'm not guaranteed that my program won't index out of bounds.
If you actually come up with a proof, you are completely guaranteed that the proven statement is true.
> Formals proofs have errors in them all the time.
Correction: Purported proofs often actually aren't proofs. It is not a proof if it is wrong.
> I want dynamic checks to catch me in those cases.
Thanks for making my point for me! Self-quotes are decidedly not tasteful, but this situation calls for a reminder:
> It is useful (again, according to proponents, not me) to consider these inconsistent attempts valid programs so that programmers can obtain example-based feedback about the consequences of their designs. Logic and abstract reasoning are not everyone's forte, after all.
Anyhow. Back to your last comment:
> Further to the point, let me reiterate: programmers do not (in almost all cases) write these proofs you are talking about.
This is just a statement of fact, which is true, indeed. But it doesn't support your original position in any way.
Yes, in the strictest sense an incorrect proof is not a proof. But at the same time, people often call either flawed proofs or purported proofs formal proofs in a looser sense. You cannot be unaware of this point. You must have understood what was being conveyed. Yet, instead you decided to engage in a nitpick over the meaning of the phrase "formal proof"
Furthermore, your claim that "If you actually come up with a proof, you are completely guaranteed that the proven statement is true." is utterly unhelpful. You know that my point was that a manually verified proof might still be wrong. And yet rather than addressing that point you decide to evade it by an ill-considered nit pick on whether an incorrect proof is still a proof.
So at this point, you are not discussing the questions in good faith, and I'm done with this conversation.
(And no, I'm not backing off my position.)
They are wrong. A purported proof is only a proof if it is actually correct. If you cannot reliably come up with a proof, not mere purported proofs, then just be honest and say so. We are not in a consultant-client relationship, so you gain nothing by lying about your skills to me.
> You know that my point was that a manually verified proof might still be wrong.
Only if you cannot reliably come up with correct proofs.
> And yet rather than addressing that point you decide to evade it by an ill-considered nit pick on whether an incorrect proof is still a proof.
It is not an “ill-considered nitpick”. It is essential to my point. If you can prove that your assertions hold, you do not need to check them dynamically. (Of course, this is logically a triviality, and it is awful that I need to explicitly make this point.)
The purpose of HN is to gratify intellectual curiosity, not smite readers with the same harangues over and over again. If you don't want to be banned, you're welcome to email hn@ycombinator.com and give us reason to believe that you'll use the site as intended in the future.