6 ms·

We have some formal verification, it's called typed systems. Very limited, I know. But some people are still praising dynamically typed languages for their "spe

We have some formal verification, it's called typed systems. Very limited, I know. But some people are still praising dynamically typed languages for their "speed" and "lack of compiler errors".

NoGravitas 9y ago
When you talk about static typing as providing some form of formal verification, you really can only talk about languages with advanced type systems like Haskell. Type systems like those in Java and C# give you very little formal verification (and I say this as someone who programs daily in C# for work and Python and Common Lisp for fun). What Java-like type systems give you is confidence in refactoring, which is not nothing, but it is not formal verification. (I'll also say that type inference and generic types in C# give me about 80% of what dynamic types in Python give me. The main thing I miss is heterogeneous tuples, which in C# have to be of type Object, or defined as structs/classes, which is too verbose for the job.)
- golergka 9y ago
  I work with C# full-time and it's type system constantly helps me. Of course, it's not Haskell or Rust, but it is still so much better than my Javascript experience. Anonymous types, generic containers and interfaces are usually enough for my needs. Can you please go into some detail about heterogenous tuples in Python? I've never used it to build big long-lasting systems so I be not aware of some of it's type capabilities.
  - pka 9y ago
    Tuples are just two or more values with separate types lumped together, i.e. (Int, String). For example, in Haskell, to get the elements of a map, there's this function: assocs :: Map k v -> [(k, v)] which gives you an array of tuples, the first element of which is of type k (the map key type) and the second element being of type v (the map value type.)
    - golergka 9y ago
      I asked a question because I assumed that I might not know something about it, since C# has Tuple<T1, T2> generic class just for that and if it would be just that, Python would have nothing on C# in that regard. But your comment is exactly what I was thinking about. So, is there something else in Python that is not present in C#?
      - pka 9y ago
        I doubt it, other than syntactic sugar, which makes tuples really easy to use, like destructuring and construction. I.e. in Python, if you have a function that returns a tuple: a, b = f(xxx) To create a tuple you just do (a, b). In Haskell, you get some other benefits, like tuples being functors (i.e. "things that can be mapped over"): map show ("tuple", 5) == ("tuple", "5") P.S. Not a Python expert, but I think tuples might be enumerable in Python, which works because Python is dynamically typed.
        klibertp 9y ago
        > Not a Python expert, but I think tuples might be enumerable in Python Yes, they are. More generally, they are sequences and they support indexing, so they are also iterable. In other words, this Python code works: list(map(str, ("tuple", 5, {}))) == ["tuple", "5", "{}"] There is also a variant of a tuple which assigns names to its positions - it's also iterable. They are also allowed to have any length. Other than that, I'm not aware of any superpowers of Python tuples.
- naasking 9y ago
  > Type systems like those in Java and C# give you very little formal verification [...] What Java-like type systems give you is confidence in refactoring, which is not nothing, but it is not formal verification. You might be surprised to hear that you can prove a large class of programs correct using plain ol' Java types [1]. [1] http://lambda-the-ultimate.org/node/5387 http://lambda-the-ultimate.org/node/5387
ajurna 9y ago
Good to see the strict typing of C has saved it from most security issues. i think it it is quite facetious to put it down to type systems.
- mpartel 9y ago
  C does not have particularly strict typing
- golergka 9y ago
  There are different type systems (think C vs Rust), and having one is always better than having none. C still prevents some issues you can have with assembly.
- naasking 9y ago
  An unsound type system doesn't prove anything about type systems. Doubly so if you don't actually use types and you're just exploiting that unsoundness with pervasive casting.
flavio81 9y ago
>We have some formal verification, it's called typed systems. Very limited, I know. Very limited. In my many years of experience doing software professionally, the serious bugs, that is, the ones that took us more than one day of debugging (after such a bug was able to be reproduced), were the ones that had nothing to do with types but with * bad understanding of the business rules * bad fundamental implementation of the problem domain * misuse / incorrect use of an API or libraries * API/library behaviour different from what the documentation says. No type system will save you from them. Type systems don't verify how the code does the correct thing. They only verify that the types moved between functions/modules satisfy certain conditions. Big deal. Where code reusability implies that your functions should apply to the widest type of circumstances (and thus increasing the scope in which they can be reused), type systems go fundamentally against to this goal, enforcing your functions to go very specific on what they're able to accept and return. Dynamically typed systems allow for faster coding, and also allow for interactive development which allows for faster, easier testing of individual components as they are developed. Also, the very best dynamically typed systems also allow for redefining / uploading updated function definitions while the code is running, which greatly increases development & testing speed (emphasis added.) This is not just a claim, this is my personal experience after about 23 years of programming where 90% of those years were spent using statically typed systems. As for speed, for highly optimized code Java, Haskell, and F# are basically in the same ballpark. Which is, very good speed. Well, Common Lisp (dynamically typed language) is not only in the same ballpark, but faster than them in some cases. You know what i'm going to choose. Or, different take on this: If i was going for absolute speed i'd be hacking in C, where no Hindley-Milner type checker gets in the way of clever tricks for gaining that extra bit of performance you need on that tight loop.
- golergka 9y ago
  > In my many years of experience doing software professionally, the serious bugs... > This is not just a claim, this is my personal experience after about 23 years of programming where 90% of those years were spent using statically typed systems. If most of your experience was with statically typed systems, it's just logical you would have very little experience with bugs that are prevented by statically typed systems - because this prevention would be at work. Looks like an opposite of survivor's fallacy, really.

We have some formal verification, it's called typed systems. Very limited, I know. But some people are still praising dynamically typed languages for their "speed" and "lack of compiler errors".

NoGravitas 9y ago

When you talk about static typing as providing some form of formal verification, you really can only talk about languages with advanced type systems like Haskell. Type systems like those in Java and C# give you very little formal verification (and I say this as someone who programs daily in C# for work and Python and Common Lisp for fun). What Java-like type systems give you is confidence in refactoring, which is not nothing, but it is not formal verification. (I'll also say that type inference and generic types in C# give me about 80% of what dynamic types in Python give me. The main thing I miss is heterogeneous tuples, which in C# have to be of type Object, or defined as structs/classes, which is too verbose for the job.)

golergka 9y ago
I work with C# full-time and it's type system constantly helps me. Of course, it's not Haskell or Rust, but it is still so much better than my Javascript experience. Anonymous types, generic containers and interfaces are usually enough for my needs. Can you please go into some detail about heterogenous tuples in Python? I've never used it to build big long-lasting systems so I be not aware of some of it's type capabilities.
- pka 9y ago
  Tuples are just two or more values with separate types lumped together, i.e. (Int, String). For example, in Haskell, to get the elements of a map, there's this function: assocs :: Map k v -> [(k, v)] which gives you an array of tuples, the first element of which is of type k (the map key type) and the second element being of type v (the map value type.)
  - golergka 9y ago
    I asked a question because I assumed that I might not know something about it, since C# has Tuple<T1, T2> generic class just for that and if it would be just that, Python would have nothing on C# in that regard. But your comment is exactly what I was thinking about. So, is there something else in Python that is not present in C#?
    - pka 9y ago
      I doubt it, other than syntactic sugar, which makes tuples really easy to use, like destructuring and construction. I.e. in Python, if you have a function that returns a tuple: a, b = f(xxx) To create a tuple you just do (a, b). In Haskell, you get some other benefits, like tuples being functors (i.e. "things that can be mapped over"): map show ("tuple", 5) == ("tuple", "5") P.S. Not a Python expert, but I think tuples might be enumerable in Python, which works because Python is dynamically typed.
      - klibertp 9y ago
        > Not a Python expert, but I think tuples might be enumerable in Python Yes, they are. More generally, they are sequences and they support indexing, so they are also iterable. In other words, this Python code works: list(map(str, ("tuple", 5, {}))) == ["tuple", "5", "{}"] There is also a variant of a tuple which assigns names to its positions - it's also iterable. They are also allowed to have any length. Other than that, I'm not aware of any superpowers of Python tuples.
naasking 9y ago
> Type systems like those in Java and C# give you very little formal verification [...] What Java-like type systems give you is confidence in refactoring, which is not nothing, but it is not formal verification. You might be surprised to hear that you can prove a large class of programs correct using plain ol' Java types [1]. [1] http://lambda-the-ultimate.org/node/5387 http://lambda-the-ultimate.org/node/5387

ajurna 9y ago

Good to see the strict typing of C has saved it from most security issues. i think it it is quite facetious to put it down to type systems.

mpartel 9y ago
C does not have particularly strict typing
golergka 9y ago
There are different type systems (think C vs Rust), and having one is always better than having none. C still prevents some issues you can have with assembly.
naasking 9y ago
An unsound type system doesn't prove anything about type systems. Doubly so if you don't actually use types and you're just exploiting that unsoundness with pervasive casting.

flavio81 9y ago

>We have some formal verification, it's called typed systems. Very limited, I know. Very limited. In my many years of experience doing software professionally, the serious bugs, that is, the ones that took us more than one day of debugging (after such a bug was able to be reproduced), were the ones that had nothing to do with types but with * bad understanding of the business rules * bad fundamental implementation of the problem domain * misuse / incorrect use of an API or libraries * API/library behaviour different from what the documentation says. No type system will save you from them. Type systems don't verify how the code does the correct thing. They only verify that the types moved between functions/modules satisfy certain conditions. Big deal. Where code reusability implies that your functions should apply to the widest type of circumstances (and thus increasing the scope in which they can be reused), type systems go fundamentally against to this goal, enforcing your functions to go very specific on what they're able to accept and return. Dynamically typed systems allow for faster coding, and also allow for interactive development which allows for faster, easier testing of individual components as they are developed. Also, the very best dynamically typed systems also allow for redefining / uploading updated function definitions while the code is running, which greatly increases development & testing speed (emphasis added.) This is not just a claim, this is my personal experience after about 23 years of programming where 90% of those years were spent using statically typed systems. As for speed, for highly optimized code Java, Haskell, and F# are basically in the same ballpark. Which is, very good speed. Well, Common Lisp (dynamically typed language) is not only in the same ballpark, but faster than them in some cases. You know what i'm going to choose. Or, different take on this: If i was going for absolute speed i'd be hacking in C, where no Hindley-Milner type checker gets in the way of clever tricks for gaining that extra bit of performance you need on that tight loop.

golergka 9y ago
> In my many years of experience doing software professionally, the serious bugs... > This is not just a claim, this is my personal experience after about 23 years of programming where 90% of those years were spent using statically typed systems. If most of your experience was with statically typed systems, it's just logical you would have very little experience with bugs that are prevented by statically typed systems - because this prevention would be at work. Looks like an opposite of survivor's fallacy, really.