4 ms·

Let me add a 3rd. 3. The program is incorrect but correct for all expected end user inputs.

naasking 4y ago
In that case, add a type that constrains the values to the expected user inputs. Now not only are you passing the type checking, you're strongly enforced this invariant at the point where it makes the most sense, you've future-proofed this code against possible future misuse where the expected inputs might change, and you've made the code essentially self-documenting.
- lliamander 4y ago
  That is the correct end state, but there can be practical considerations for why you might want to run (and possibly even release) the software in this partially correct state, and fix the edge cases later.
  - naasking 4y ago
    I don't disagree, but most statically typed languages don't enforce a level of correctness where this would be an issue. We're not programming with theorem provers with an elaborate specification. I somewhat agree with your point #2 which is why Haskell provides a deferred type checking mode for prototyping purposes[1]. I think this should be more common among typed languages, but this is not a very typical scenario either. [1] https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/defer_type_errors.html https://downloads.haskell.org/ghc/latest/docs/users_guide/ex...
- ReflectedImage 4y ago
  I'm not sure many languages support the introduction of types such as: * An integer that is sum of two primes. * A string that is created between the hours of 2 pm - 4 pm on a Tuesday. * A dictionary who's fields comprise a valid tax return. What do you mean by future proving? If the new version of the code doesn't ship by 2 pm today, the company goes bankrupt and there is no future for the code.
  - naasking 4y ago
    > I'm not sure many languages support the introduction of types such as: Any language with types can enforce any proposition you can reliably check, which you run as part of the type's constructor. There are multiple ways to do this, for instance in pseudo-ML: > * An integer that is sum of two primes. type SumOfPrimes fn sumOfPrimes : Prime -> Prime -> SumOfPrimes type Prime fn primeOfInt : Int -> Maybe Prime > * A string that is created between the hours of 2 pm - 4 pm on a Tuesday. type Tuesday2To4String fn whichString : Clock -> String -> Either String Tuesday2To4String > * A dictionary who's fields comprise a valid tax return. type ValidTaxReturn fn checkTaxReturn : Dictionary String String -> Maybe ValidTaxReturn > What do you mean by future proving? If the new version of the code doesn't ship by 2 pm today, the company goes bankrupt and there is no future for the code. Shipping broken code will not save the company from bankruptcy. It's also a myth that dynamically typed languages will get your code out faster.
    - ReflectedImage 4y ago
      I'm not sure how you intend to check the creation date of a string in memory since there is no information available to do that or that a tax return is valid given the thousands of rules involved. Nevertheless let's move on. It's not a myth, if you are using dynamic typing you will get three times the number of features out the door as someone who uses static typing. It's just a fact. 1 dynamic typed programmer = 3 static typed programmers in productivity and output. That is why people use dynamic typing. From a commerical perspective, static typing does not make sense in most cases. You need something more than a typical business CRUD app to justify it. Usually you only need static typing for performance reasons. Like for a video game or image processing. In practice, the shipped code doesn't have noticably more bugs. That just something which people who have never used dynamic typing properly like to believe. If you ever read an article by Eve online where they say Python is their secret weapon or watched what Discord did by implementing everything in Python first. You will understand.
      - naasking 4y ago
        > I'm not sure how you intend to check the creation date of a string in memory since there is no information available to do that See the signature of the constructor function I provided. > or that a tax return is valid given the thousands of rules involved. Tax software does it every year. Clearly the government has an effective procedure to decide the validity of a tax return, even if that procedure is executed by a human. > It's not a myth, if you are using dynamic typing you will get three times the number of features out the door as someone who uses static typing. It's just a fact. That's just laughably false. There is zero empirical evidence supporting this claim. > In practice, the shipped code doesn't have noticably more bugs. That just something which people who have never used dynamic typing properly like to believe. No True Scotsman fallacy.

In that case, add a type that constrains the values to the expected user inputs. Now not only are you passing the type checking, you're strongly enforced this invariant at the point where it makes the most sense, you've future-proofed this code against possible future misuse where the expected inputs might change, and you've made the code essentially self-documenting.

lliamander 4y ago
That is the correct end state, but there can be practical considerations for why you might want to run (and possibly even release) the software in this partially correct state, and fix the edge cases later.
- naasking 4y ago
  I don't disagree, but most statically typed languages don't enforce a level of correctness where this would be an issue. We're not programming with theorem provers with an elaborate specification. I somewhat agree with your point #2 which is why Haskell provides a deferred type checking mode for prototyping purposes[1]. I think this should be more common among typed languages, but this is not a very typical scenario either. [1] https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/defer_type_errors.html https://downloads.haskell.org/ghc/latest/docs/users_guide/ex...
ReflectedImage 4y ago
I'm not sure many languages support the introduction of types such as: * An integer that is sum of two primes. * A string that is created between the hours of 2 pm - 4 pm on a Tuesday. * A dictionary who's fields comprise a valid tax return. What do you mean by future proving? If the new version of the code doesn't ship by 2 pm today, the company goes bankrupt and there is no future for the code.
- naasking 4y ago
  > I'm not sure many languages support the introduction of types such as: Any language with types can enforce any proposition you can reliably check, which you run as part of the type's constructor. There are multiple ways to do this, for instance in pseudo-ML: > * An integer that is sum of two primes. type SumOfPrimes fn sumOfPrimes : Prime -> Prime -> SumOfPrimes type Prime fn primeOfInt : Int -> Maybe Prime > * A string that is created between the hours of 2 pm - 4 pm on a Tuesday. type Tuesday2To4String fn whichString : Clock -> String -> Either String Tuesday2To4String > * A dictionary who's fields comprise a valid tax return. type ValidTaxReturn fn checkTaxReturn : Dictionary String String -> Maybe ValidTaxReturn > What do you mean by future proving? If the new version of the code doesn't ship by 2 pm today, the company goes bankrupt and there is no future for the code. Shipping broken code will not save the company from bankruptcy. It's also a myth that dynamically typed languages will get your code out faster.
  - ReflectedImage 4y ago
    I'm not sure how you intend to check the creation date of a string in memory since there is no information available to do that or that a tax return is valid given the thousands of rules involved. Nevertheless let's move on. It's not a myth, if you are using dynamic typing you will get three times the number of features out the door as someone who uses static typing. It's just a fact. 1 dynamic typed programmer = 3 static typed programmers in productivity and output. That is why people use dynamic typing. From a commerical perspective, static typing does not make sense in most cases. You need something more than a typical business CRUD app to justify it. Usually you only need static typing for performance reasons. Like for a video game or image processing. In practice, the shipped code doesn't have noticably more bugs. That just something which people who have never used dynamic typing properly like to believe. If you ever read an article by Eve online where they say Python is their secret weapon or watched what Discord did by implementing everything in Python first. You will understand.
    - naasking 4y ago
      > I'm not sure how you intend to check the creation date of a string in memory since there is no information available to do that See the signature of the constructor function I provided. > or that a tax return is valid given the thousands of rules involved. Tax software does it every year. Clearly the government has an effective procedure to decide the validity of a tax return, even if that procedure is executed by a human. > It's not a myth, if you are using dynamic typing you will get three times the number of features out the door as someone who uses static typing. It's just a fact. That's just laughably false. There is zero empirical evidence supporting this claim. > In practice, the shipped code doesn't have noticably more bugs. That just something which people who have never used dynamic typing properly like to believe. No True Scotsman fallacy.