5 ms·

You can only deem it obvious if you can actually prove it. --- @winstonewert > True, but the key word is "can". I could write a proof that my dynamically typ

You can only deem it obvious if you can actually prove it. --- @winstonewert > True, but the key word is "can". I could write a proof that my dynamically typed programs are correct If you could actually write the proof, then you would not want the dynamic checks, as all they offer is protection against errors that you can prove you have not made. > or that my functions do not index out of bounds, but I don't. Are you actually sure you can? --- @AnimalMuppet > By a certain point, you've seen enough of them that you don't have to prove it, you can just see it. If all your loops are so similar to each other that you can “just see” that an iteration pattern is correct, you should consider writing an iterator library, so that others can benefit from your hard-earned wisdom without going through the pain themselves. Or else, if you are implying that you could be given an arbitrary loop and “just see” that it is correct, I am afraid you are wrong. > But of course, everybody thinks they're at that point well before they actually are... I have never even entertained the possibility.

AnimalMuppet 8y ago
I disagree. I've been programming professionally for 33 years. I may have written one wrongly-indexed "for" loop in the last 10 years. By a certain point, you've seen enough of them that you don't have to prove it, you can just see it. But of course, everybody thinks they're at that point well before they actually are...
winstonewert 8y ago
True, but the key word is "can". I could write a proof that my dynamically typed programs are correct or that my functions do not index out of bounds, but I don't. Nor has any programmer I've ever worked with. Nor has any open source project I've ever seen provide such proofs. People do not write these imaginary proofs, because it would be a waste of time.
winstonewert 8y ago
> If you could actually write the proof, then you would not want the dynamic checks, as all they offer is protection against errors that you can prove you have not made. 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.
- catnaroek 8y ago
  Yes! This is the nice moment when the other party in the debate starts to back off from their original position, which, I shall remind you, was: > 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.
  - winstonewert 8y ago
    > Correction: Purported formal proofs often actually aren't formal proofs. It is not a proof if it is wrong. 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.)

AnimalMuppet 8y ago

I disagree. I've been programming professionally for 33 years. I may have written one wrongly-indexed "for" loop in the last 10 years. By a certain point, you've seen enough of them that you don't have to prove it, you can just see it. But of course, everybody thinks they're at that point well before they actually are...

winstonewert 8y ago

True, but the key word is "can". I could write a proof that my dynamically typed programs are correct or that my functions do not index out of bounds, but I don't. Nor has any programmer I've ever worked with. Nor has any open source project I've ever seen provide such proofs. People do not write these imaginary proofs, because it would be a waste of time.

winstonewert 8y ago

> If you could actually write the proof, then you would not want the dynamic checks, as all they offer is protection against errors that you can prove you have not made. 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.

catnaroek 8y ago
Yes! This is the nice moment when the other party in the debate starts to back off from their original position, which, I shall remind you, was: > 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.
- winstonewert 8y ago
  > Correction: Purported formal proofs often actually aren't formal proofs. It is not a proof if it is wrong. 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.)