• Digital Mark
    link
    fedilink
    English
    arrow-up
    2
    arrow-down
    5
    ·
    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
        link
        fedilink
        English
        arrow-up
        2
        arrow-down
        1
        ·
        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…