• colonial@lemmy.world
    link
    fedilink
    arrow-up
    14
    arrow-down
    1
    ·
    edit-2
    1 year ago

    No matter how many unit tests or comments you write, it’s impossible to “prove” type correctness in a dynamically typed language - and it will eventually blow up in your face when you have to refactor. There’s a reason for the adage “testing can’t prove the absence of bugs.”

    People like static typing because it offers strong guarantees and eliminates entire classes of bullshit bugs, not because they’re “weak minded.”

    • Digital Mark@lemmy.ml
      link
      fedilink
      English
      arrow-up
      2
      arrow-down
      4
      ·
      1 year ago

      Typing can’t prove anything, either. It just creates bugs and crashes.

      Your program logic is the part that will not be fixed by it.

      • colonial@lemmy.world
        link
        fedilink
        arrow-up
        6
        arrow-down
        1
        ·
        edit-2
        1 year ago

        Typing can’t prove anything, either.

        Incorrect. Static typing can prove many things, depending on the quality of the type system.

        At the very least, it proves that your data is organized, stored, passed around and used in a logically valid and consistent manner. Make that proof impossible, and the compiler complains. (And with good reason - it doesn’t matter how good your program logic is if you’re feeding it bad data. Garbage in, garbage - or a runtime error - out.)

        In a dynamically typed language, your program logic still implicitly depends on that proof holding - it’s just that you, the fallible human, has to make sure everything checks out. Python added type hints for precisely this reason.

        Additionally, with more advanced static type systems, it becomes possible to issue guarantees beyond simple type safety. Patterns like typestate (found in TS, Haskell and Rust, off the top of my head) can be used to make illegal states unrepresentable at compile time. Try to write to a closed file or make an invalid state machine transition? The compiler will see it and say no.

        It just creates bugs and crashes.

        In what universe are runtime errors turned compile-time errors a source of bugs and crashes? A statically-typed program won’t blow up in production because some poor intern wasn’t able to keep the implicit type bounds of every single function parameter in his head.

        • Digital Mark@lemmy.ml
          link
          fedilink
          English
          arrow-up
          2
          ·
          1 year ago

          There’s some math & CS papers you should read, Gödel’s incompleteness theorem, Turing’s halting problem. YOU CANNOT prove your way out of logic errors. You cannot make a universal type system. All you’re doing is wasting time with false confidence.

          • colonial@lemmy.world
            link
            fedilink
            arrow-up
            2
            arrow-down
            1
            ·
            1 year ago

            I never said that static typing stops all logic errors or fully proves program correctness, but go off I guess…