6 ms·

> Those that have caused space ships to explode It's funny you should mention this, as it immediately brings [1] to my mind. This well-known incident was due t

> Those that have caused space ships to explode It's funny you should mention this, as it immediately brings [1] to my mind. This well-known incident was due to type-checking, with acceptable ranges defined ahead of time for some types (which resonates with your comment: make birthdayGreeting accept ranges 1-150 or something, easy to do in ADA). There are a few more well-publicized issues with spacecraft that could have been caught with better type-checking, including metric/imperial conversions (why not build the unit into a type? Though the fault probably was with integration testing for [2]). Of course, you are right that type checking can't find every code issue (especially algorithmic), it doesn't replace tests. Instant feedback and type hints are invaluable during the development phase, though. In your example, one could probably replace the first name string by a person type/object, by the way. [1]: https://en.m.wikipedia.org/wiki/Ariane_flight_V88 https://en.m.wikipedia.org/wiki/Ariane_flight_V88 [2]: https://en.m.wikipedia.org/wiki/Mars_Climate_Orbiter https://en.m.wikipedia.org/wiki/Mars_Climate_Orbiter

bjourne 3y ago
Neither of those were "bona fide type errors". The fact that both errors ocurred while using statically typed languages shows that. The orbiter failed because inches were interpreted as centimeters. But as both datums were stored as floating point numbers, which they always would be, in any reasonable implementation, static typing wouldn't have caught anything. The Ariane failure was due to a cast of a double to a short resuling in an overflow. Again, not something static typing can catch because it can't statically check the value of an arbitrary double. No, even more types is not the solution. It's not pratical to wrap every measurement in a Meter or Inch type (standardization is one issue, is my Meter type the same as your Meter type?) and it doesn't significantly increase the amount of invariants checked. You still have range issues and you still won't get a statically check PrimeNumber type. I'm not familiar with ADA, but VHDL has similar range constraints which are runtime checked.
- thfuran 3y ago
  >But as both datums were stored as floating point numbers, which they always would be, in any reasonable implementation It doesn't strike me as inherently unreasonable to use fixed point. At any rate, there are languages with built-in unit systems, so you could declare something like float length = 4.5 <m> and get an error if you try to add it to something in a different unit without having to roll your own dimensional analysis framework.
  - bjourne 3y ago
    Of course, fixed point would have been a reasonable choice too. But here is my point. Someone who likes testing could say "This bug would have been caught with better testing". Someone who likes static typing could say "This bug would have been caught if they had used an esoteric type system with support for physical quantities." ... Which no one uses. Thus, you have an argument between something real and realistic, and something imagined and unrealistic.
    - thfuran 3y ago
      That you aren't familiar with something hardly makes it imaginary. That exact formulation of unit system is, I think, pretty uncommon, but there are widely used languages (vhdl) where uniting is more directly part of the type system and widely used uniting systems as libraries (boost) where it is not directly a language feature.
      - bjourne 3y ago
        VHDL physical types are nothing more than annotated integers. Making them completely useless for general arithmetic. You could not use them for converting from say Celsius to Fahrenheiht. It's cute that you bring up Boost which contains everything and the kitchen sink as evidence of "widely used". Show me a 3d engine that uses physical units for distance calculations. No one does it because it is a horrible idea.
    - HideousKojima 3y ago
      How about "This bug would have been caught if instead of storing the distance in a float, they stored it in a struct/class that also contained an enum defining the units". Just about any language could handle that.
- vouwfietsman 3y ago
  > The fact that both errors ocurred while using statically typed languages shows that Obviously it doesn't, since you can make a statically typed language program where every variable is a string map and every function takes variable args, and have no help from your compiler at any time because every type is always the right type. Sounds stupid, but in fact this is what happened in the examples. The examples are bona fide type errors, because even though a statically typed language is used, multiple different types of numbers got the same static type causing the issue. So the people here were offered the solution to their problem from their domain (two types of numbers), choose to use dynamic typing (make both a float even though they're different things), causing the compiler to have no way of statically checking their code, and that caused a bug. It's the opposite of a counter example. It is in fact the absence of enough typing that caused these issues. How much more typing do you need :)
  - Draiken 3y ago
    In other words: types were not a deciding factor. Ultimately bugs cannot be prevented by having a type system. We make mistakes regardless of static or dynamic types. We can argue it's because of the lack of types, tests, oversight and so on. I'd argue nothing can force a programmer to design a perfect system. >The examples are bona fide type errors I'd disagree because those are logical errors. You can represent those as different types with a type system, but you could also not use a type system and convert those values properly. Whether we represent them as different types or not is an implementation choice. Those can be considered "type errors" (or missing types? a type of primitive obsession?) in a typed language. But it's still an issue with the implementation's logic.
    - vouwfietsman 3y ago
      In other words: the seatbelt is not a deciding factor. Ultimately deaths cannot be prevented by seatbelts. People will die regardless whether they wear a seatbelt or not. We can argue its because of a lack of seatbelts, roll cages, airbags and so on. I'd argue nothing can force force a person to be perfectly safe while driving. > The examples are bona fide safety issues I'd disagree because those are driving errors. You can present those as cars missing safety features, but you could also not use those safety systems and just drive carefully. Whether we use safety systems or not is a design choice. Those can be considered "safety issues" (or missing safety? a type of safety obsession?) in a safety design perspective. But it's still an issue with the driver's behavior. bit of hyperbole for flavour: If we could just ditch the heavy roll cage, we could go much faster!
- nyssos 3y ago
  > But as both datums were stored as floating point numbers, which they always would be, in any reasonable implementation, static typing wouldn't have caught anything. Types are not runtime representations, and any good nominal type system will allow you to avoid this sort of problem easily. For example, this Haskell code newtype Inches = Inches Double deriving Num newtype Centimeters = Centimeters Double deriving Num a :: Centimeters a = Centimeters 1.0 b :: Inches b = Inches 1.0 fine = a + a alsoFine = b + b mistake = a + b will give this type error Couldn't match expected type ‘Centimeters’ with actual type ‘Inches’ In the second argument of ‘(+)’, namely ‘b’ In the expression: a + b In an equation for ‘mistake’: mistake = a + b but both `a` and `b` will be doubles at runtime.
  - bjourne 3y ago
    That is why I wrote "in any reasonable implementation". Embedding physical quantities in the type system is possible in many language but is not practical. Hence why safety-critical software doesn't contain declarations like yours. For example, what is the type of Inch * Inch? What is the type of Inch / Inch? Sure, perhaps if NASA and their subcontractors had used a common well-developed physical quantities library then the bug could have been caught during compile-time. But I think it is a moot point since most people don't use such libraries.
    - esafak 3y ago
      > For example, what is the type of Inch * Inch? An area, inch^2. > What is the type of Inch / Inch? A unitless ratio? I don't understand why this is not practical in safety-critical software. nyssos demonstrated what I believe is the right way to do it.
      - bjourne 3y ago
        These semantics make the type incompatible with the Num class and attempting to plug your type into, say, a run of the mill ode solver likely won't do what you want. So you have two options. 1) Rewrite all code to become "quantity aware". Multiplying two Matrix[Inch] results in a Matrix[Inch2] and so on. 2) Litter your code with floatToInch and inchToFloat conversions. I think you can see why both options suck? If you really can't, then perhaps try finding some safety-critical software that relies on "physical quantity types" in some form or another?
- freilanzer 3y ago
  > The orbiter failed because inches were interpreted as centimeters. But as both datums were stored as floating point numbers, which they always would be, in any reasonable implementation, static typing wouldn't have caught anything. They would not always be stored as flat floats. You could have type aliases for both values (type alias inch = float, the same for cm) and have not a flat float but an inch or cm as a type. Or, even better, F# has type support for such values: https://learn.microsoft.com/en-us/dotnet/fsharp/language-reference/units-of-measure https://learn.microsoft.com/en-us/dotnet/fsharp/language-ref...

bjourne 3y ago

Neither of those were "bona fide type errors". The fact that both errors ocurred while using statically typed languages shows that. The orbiter failed because inches were interpreted as centimeters. But as both datums were stored as floating point numbers, which they always would be, in any reasonable implementation, static typing wouldn't have caught anything. The Ariane failure was due to a cast of a double to a short resuling in an overflow. Again, not something static typing can catch because it can't statically check the value of an arbitrary double. No, even more types is not the solution. It's not pratical to wrap every measurement in a Meter or Inch type (standardization is one issue, is my Meter type the same as your Meter type?) and it doesn't significantly increase the amount of invariants checked. You still have range issues and you still won't get a statically check PrimeNumber type. I'm not familiar with ADA, but VHDL has similar range constraints which are runtime checked.

thfuran 3y ago
>But as both datums were stored as floating point numbers, which they always would be, in any reasonable implementation It doesn't strike me as inherently unreasonable to use fixed point. At any rate, there are languages with built-in unit systems, so you could declare something like float length = 4.5 <m> and get an error if you try to add it to something in a different unit without having to roll your own dimensional analysis framework.
- bjourne 3y ago
  Of course, fixed point would have been a reasonable choice too. But here is my point. Someone who likes testing could say "This bug would have been caught with better testing". Someone who likes static typing could say "This bug would have been caught if they had used an esoteric type system with support for physical quantities." ... Which no one uses. Thus, you have an argument between something real and realistic, and something imagined and unrealistic.
  - thfuran 3y ago
    That you aren't familiar with something hardly makes it imaginary. That exact formulation of unit system is, I think, pretty uncommon, but there are widely used languages (vhdl) where uniting is more directly part of the type system and widely used uniting systems as libraries (boost) where it is not directly a language feature.
    - bjourne 3y ago
      VHDL physical types are nothing more than annotated integers. Making them completely useless for general arithmetic. You could not use them for converting from say Celsius to Fahrenheiht. It's cute that you bring up Boost which contains everything and the kitchen sink as evidence of "widely used". Show me a 3d engine that uses physical units for distance calculations. No one does it because it is a horrible idea.
  - HideousKojima 3y ago
    How about "This bug would have been caught if instead of storing the distance in a float, they stored it in a struct/class that also contained an enum defining the units". Just about any language could handle that.
vouwfietsman 3y ago
> The fact that both errors ocurred while using statically typed languages shows that Obviously it doesn't, since you can make a statically typed language program where every variable is a string map and every function takes variable args, and have no help from your compiler at any time because every type is always the right type. Sounds stupid, but in fact this is what happened in the examples. The examples are bona fide type errors, because even though a statically typed language is used, multiple different types of numbers got the same static type causing the issue. So the people here were offered the solution to their problem from their domain (two types of numbers), choose to use dynamic typing (make both a float even though they're different things), causing the compiler to have no way of statically checking their code, and that caused a bug. It's the opposite of a counter example. It is in fact the absence of enough typing that caused these issues. How much more typing do you need :)
- Draiken 3y ago
  In other words: types were not a deciding factor. Ultimately bugs cannot be prevented by having a type system. We make mistakes regardless of static or dynamic types. We can argue it's because of the lack of types, tests, oversight and so on. I'd argue nothing can force a programmer to design a perfect system. >The examples are bona fide type errors I'd disagree because those are logical errors. You can represent those as different types with a type system, but you could also not use a type system and convert those values properly. Whether we represent them as different types or not is an implementation choice. Those can be considered "type errors" (or missing types? a type of primitive obsession?) in a typed language. But it's still an issue with the implementation's logic.
  - vouwfietsman 3y ago
    In other words: the seatbelt is not a deciding factor. Ultimately deaths cannot be prevented by seatbelts. People will die regardless whether they wear a seatbelt or not. We can argue its because of a lack of seatbelts, roll cages, airbags and so on. I'd argue nothing can force force a person to be perfectly safe while driving. > The examples are bona fide safety issues I'd disagree because those are driving errors. You can present those as cars missing safety features, but you could also not use those safety systems and just drive carefully. Whether we use safety systems or not is a design choice. Those can be considered "safety issues" (or missing safety? a type of safety obsession?) in a safety design perspective. But it's still an issue with the driver's behavior. bit of hyperbole for flavour: If we could just ditch the heavy roll cage, we could go much faster!
nyssos 3y ago
> But as both datums were stored as floating point numbers, which they always would be, in any reasonable implementation, static typing wouldn't have caught anything. Types are not runtime representations, and any good nominal type system will allow you to avoid this sort of problem easily. For example, this Haskell code newtype Inches = Inches Double deriving Num newtype Centimeters = Centimeters Double deriving Num a :: Centimeters a = Centimeters 1.0 b :: Inches b = Inches 1.0 fine = a + a alsoFine = b + b mistake = a + b will give this type error Couldn't match expected type ‘Centimeters’ with actual type ‘Inches’ In the second argument of ‘(+)’, namely ‘b’ In the expression: a + b In an equation for ‘mistake’: mistake = a + b but both `a` and `b` will be doubles at runtime.
- bjourne 3y ago
  That is why I wrote "in any reasonable implementation". Embedding physical quantities in the type system is possible in many language but is not practical. Hence why safety-critical software doesn't contain declarations like yours. For example, what is the type of Inch * Inch? What is the type of Inch / Inch? Sure, perhaps if NASA and their subcontractors had used a common well-developed physical quantities library then the bug could have been caught during compile-time. But I think it is a moot point since most people don't use such libraries.
  - esafak 3y ago
    > For example, what is the type of Inch * Inch? An area, inch^2. > What is the type of Inch / Inch? A unitless ratio? I don't understand why this is not practical in safety-critical software. nyssos demonstrated what I believe is the right way to do it.
    - bjourne 3y ago
      These semantics make the type incompatible with the Num class and attempting to plug your type into, say, a run of the mill ode solver likely won't do what you want. So you have two options. 1) Rewrite all code to become "quantity aware". Multiplying two Matrix[Inch] results in a Matrix[Inch2] and so on. 2) Litter your code with floatToInch and inchToFloat conversions. I think you can see why both options suck? If you really can't, then perhaps try finding some safety-critical software that relies on "physical quantity types" in some form or another?
freilanzer 3y ago
> The orbiter failed because inches were interpreted as centimeters. But as both datums were stored as floating point numbers, which they always would be, in any reasonable implementation, static typing wouldn't have caught anything. They would not always be stored as flat floats. You could have type aliases for both values (type alias inch = float, the same for cm) and have not a flat float but an inch or cm as a type. Or, even better, F# has type support for such values: https://learn.microsoft.com/en-us/dotnet/fsharp/language-reference/units-of-measure https://learn.microsoft.com/en-us/dotnet/fsharp/language-ref...