4 ms·

The argument for dynamic typing (whether one agrees with it or not, I actually don't) has nothing to do with explicit annotations. Rather, it is that there are

The argument for dynamic typing (whether one agrees with it or not, I actually don't) has nothing to do with explicit annotations. Rather, it is that there are paths in the design space that lead to correct solutions but pass through several inconsistent attempts (i.e., containing parts that contradicting each other and/or the problem statement). 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.

zenhack 9y ago
Yeah, that's an actually reasonable argument (I don't buy it either, but it's coherent enough). But I honestly think most of the time people aren't making that argument, they're just complaining about the typed languages they know -- more often than not Java.
- mcphage 9y ago
  > they're just complaining about the typed languages they know -- more often than not Java. Java has a particularly bad type system, and it used to be even worse.
winstonewert 9y ago
I'd make yet a different account of the benefit of dynamic typing. My reasoning skills exceed that of my compiler and I can thus determine that certain designs are type-safe that my compiler cannot. This means that in static languages I end up either 1) spending a lot of time convincing the compiler my design is type-safe, 2) am restricted in the designs I can choose 3) casting types losing the advantage of static typing. With dynamic typing I'm free to just write the code. Having said that, I now really like Rust which goes all the way in the other direction.
- catnaroek 9y ago
  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.
- AnimalMuppet 9y ago
  > My reasoning skills exceed that of my compiler... Well, your reasoning skills are different from your compiler. You can see things that the compiler can't. But the compiler can also see things that you don't until the compiler points them out to you. > ... and I can thus determine that certain designs are type-safe that my compiler cannot. True. But your compiler can also see that certain things are not type-safe that you think are. Personally, I'm inclined to something like "the human can over-ride the compiler, but only after listening to it.
  - winstonewert 9y ago
    > Well, your reasoning skills are different from your compiler. Very true. > Personally, I'm inclined to something like "the human can over-ride the compiler, but only after listening to it. For me, it depends on the language. If you have generics, macros, and non-nullable types: I'm on board. If you lack any one of those, I'd rather be dynamic. I don't want to be constantly overriding the compiler, writing a lot of boilerplate, or still have to deal with nulls.

zenhack 9y ago

Yeah, that's an actually reasonable argument (I don't buy it either, but it's coherent enough). But I honestly think most of the time people aren't making that argument, they're just complaining about the typed languages they know -- more often than not Java.

mcphage 9y ago
> they're just complaining about the typed languages they know -- more often than not Java. Java has a particularly bad type system, and it used to be even worse.

winstonewert 9y ago

I'd make yet a different account of the benefit of dynamic typing. My reasoning skills exceed that of my compiler and I can thus determine that certain designs are type-safe that my compiler cannot. This means that in static languages I end up either 1) spending a lot of time convincing the compiler my design is type-safe, 2) am restricted in the designs I can choose 3) casting types losing the advantage of static typing. With dynamic typing I'm free to just write the code. Having said that, I now really like Rust which goes all the way in the other direction.

catnaroek 9y ago
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.
AnimalMuppet 9y ago
> My reasoning skills exceed that of my compiler... Well, your reasoning skills are different from your compiler. You can see things that the compiler can't. But the compiler can also see things that you don't until the compiler points them out to you. > ... and I can thus determine that certain designs are type-safe that my compiler cannot. True. But your compiler can also see that certain things are not type-safe that you think are. Personally, I'm inclined to something like "the human can over-ride the compiler, but only after listening to it.
- winstonewert 9y ago
  > Well, your reasoning skills are different from your compiler. Very true. > Personally, I'm inclined to something like "the human can over-ride the compiler, but only after listening to it. For me, it depends on the language. If you have generics, macros, and non-nullable types: I'm on board. If you lack any one of those, I'd rather be dynamic. I don't want to be constantly overriding the compiler, writing a lot of boilerplate, or still have to deal with nulls.