4 ms·

This is a very good argument against mandatory automatic static checks, so long as they are replaced with equally mandatory manual proofs, included in the progr

This is a very good argument against mandatory automatic static checks, so long as they are replaced with equally mandatory manual proofs, included in the program's comments and/or documentation. But it does not justify dynamic typing in any way. For example, most programming languages offer no way to statically verify array indexing operations, so I just get my hands dirty and prove my array indices correct the old fashioned way (brain, paper and pen). But runtime bounds checking still annoys me, because they branch on a bit whose value I know beforehand, creating an unreachable control flow path.

winstonewert 9y ago
Are you telling me that you do a formal proof on pen and paper for every array index to ensure that it is valid?
- catnaroek 9y ago
  Yes. This is the only way you can justify that you know better than the compiler.
  - winstonewert 9y ago
    So, if you wrote the following code: double sum(double[] numbers) { double total = 0.0; for (int index = 0; index < numbers.length; index++) { total += numbers[index]; } return total } You would write a formal proof on paper that the index won't go out of bounds?
    - catnaroek 9y ago
      Theorem: Whenever `numbers[index]` is used, `0 <= index < numbers.length`. Proof: Use the loop invariant `0 <= index <= numbers.length`. The invariant holds before the loop begins because `index == 0` (established by you) and `numbers.length >= 0` (established by the implementor of the array type) imply it. Inductively assume that prior iterations of the loop preserved the invariant and didn't perform any invalid indexing operations. Now, every time the loop's condition is evaluated, there are two possibilities: either `0 <= index == numbers.length` or `0 <= index < numbers.length`. In the former case, the loop terminates and no further indexing operations are used, establishing the claim. In the latter case, `numbers[index]` is a valid indexing operation, and the subsequent `index++` operation does not destroy the invariant, because, given the precondition `0 <= index < numbers.length`, the operation `index++` establishes the postcondition `0 < index <= numbers.length`, which implies the invariant. --- Note, however, that in this case it would have been more efficient to use an iterator, because the iterator's implementation already packages this proof in a reusable way, so that you don't need to reprove it every time you write a loop similar to this.
      - winstonewert 9y ago
        Well, I've never seen anyone write a proof for a function so trivial. Instead, most people will simply deem the proof to be sufficiently obvious they don't need to write one out. I've only ever seen someone offer something in terms of a proof for more complex situation where its decidely non-intuitive that array indexes will not go out of bounds.
        catnaroek 9y ago
        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 9y 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 9y 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 9y ago

Are you telling me that you do a formal proof on pen and paper for every array index to ensure that it is valid?

catnaroek 9y ago
Yes. This is the only way you can justify that you know better than the compiler.
- winstonewert 9y ago
  So, if you wrote the following code: double sum(double[] numbers) { double total = 0.0; for (int index = 0; index < numbers.length; index++) { total += numbers[index]; } return total } You would write a formal proof on paper that the index won't go out of bounds?
  - catnaroek 9y ago
    Theorem: Whenever `numbers[index]` is used, `0 <= index < numbers.length`. Proof: Use the loop invariant `0 <= index <= numbers.length`. The invariant holds before the loop begins because `index == 0` (established by you) and `numbers.length >= 0` (established by the implementor of the array type) imply it. Inductively assume that prior iterations of the loop preserved the invariant and didn't perform any invalid indexing operations. Now, every time the loop's condition is evaluated, there are two possibilities: either `0 <= index == numbers.length` or `0 <= index < numbers.length`. In the former case, the loop terminates and no further indexing operations are used, establishing the claim. In the latter case, `numbers[index]` is a valid indexing operation, and the subsequent `index++` operation does not destroy the invariant, because, given the precondition `0 <= index < numbers.length`, the operation `index++` establishes the postcondition `0 < index <= numbers.length`, which implies the invariant. --- Note, however, that in this case it would have been more efficient to use an iterator, because the iterator's implementation already packages this proof in a reusable way, so that you don't need to reprove it every time you write a loop similar to this.
    - winstonewert 9y ago
      Well, I've never seen anyone write a proof for a function so trivial. Instead, most people will simply deem the proof to be sufficiently obvious they don't need to write one out. I've only ever seen someone offer something in terms of a proof for more complex situation where its decidely non-intuitive that array indexes will not go out of bounds.
      - catnaroek 9y ago
        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 9y 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 9y 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.