Comment on We did this to ourselves

• DumbAceDragon@sh.itjust.works ⁨1⁩ ⁨year⁩ ago

  Dynamic languages were invented by runtime error companies to sell more runtime errors.

  source

  • gandalf_der_12te@feddit.de ⁨1⁩ ⁨year⁩ ago

    What

    source

    • TJmCAwesome@feddit.nu ⁨1⁩ ⁨year⁩ ago

      It’s making fun of dynamic languages because rather than letting the compiler prove theorems about statically typed code, they… don’t.

      source

      • gandalf_der_12te@feddit.de ⁨1⁩ ⁨year⁩ ago

        yeah yeah, thanks, i get it. It was more of an ironic “what”

        source

        • -> View More Comments
• deegeese@sopuli.xyz ⁨1⁩ ⁨year⁩ ago

  Turns out getting working code is a lot cheaper and more useful than formally proven code.

  source

  • tatterdemalion@programming.dev ⁨1⁩ ⁨year⁩ ago

    And a lot more bug prone. I’m just explaining the OP because people didn’t get it. I’m not saying dyanamic languages are bad. I’m saying they have different trade-offs.

    source

    • deegeese@sopuli.xyz ⁨1⁩ ⁨year⁩ ago

      The problem with formal proofs for code is that it assumes the spec/ requirements are complete and big-free.

      I find most bugs come from missed or misinterpreted requirements.

      source

      • tatterdemalion@programming.dev ⁨1⁩ ⁨year⁩ ago

        I have a feeling you are misunderstanding what is meant by “theorem” here. For example, one theorem that is proven by all safe Rust programs is that they are free of data races. That should always be a requirement for functional software. This is a more pragmatic type of automatic theorem proving that doesn’t require a direct proof from the code author. The compiler does the proof for you.

        source
  • BradleyUffner@lemmy.world ⁨1⁩ ⁨year⁩ ago

    And maintainable code is even cheaper and more useful than that in the long run.

    source

    • floofloof@lemmy.ca ⁨1⁩ ⁨year⁩ ago

      Ah, the long run. I keep trying to explain this concept to management without success.

      source
  • FiskFisk33@startrek.website ⁨1⁩ ⁨year⁩ ago

    The technical debt is strong in this one

    source

    • deegeese@sopuli.xyz ⁨1⁩ ⁨year⁩ ago

      You call it tech debt, I call it last quarter’s profits.

      source
  • Anders429@programming.dev ⁨1⁩ ⁨year⁩ ago

    Cheaper? Yes, I guess so, depending on how you measure cost. More useful? Absolutely disagree.

    source

    • deegeese@sopuli.xyz ⁨1⁩ ⁨year⁩ ago

      Industry will pick functionality over verification every time.

      source

      • Buttons@programming.dev ⁨1⁩ ⁨year⁩ ago

        Industry will leak PII without consequence every week.

        source
      • mikidep@lemmy.world ⁨9⁩ ⁨months⁩ ago

        Industry will choose not to verify that your function does not produce NullPointerException wasting hours of the client’s work, because in order to do that they would have to have actual requirements for software developers, and in order to do that they would have to 1 - have the managers be actually technically literate, and 2 - pay the developers properly That’s it. That’s the theorems. The “formal verification” we’re talking about here are those of the likes of “this value is a damn integer”, or as you could interpret it “your code is not stupidly broken”.

        To be clear, I’m not writing this big comment for you, I know you’re trolling or whatever you’re into, I’m writing this to inform other readers. ✌🏻

        source
  • sping@lemmy.sdf.org ⁨1⁩ ⁨year⁩ ago

    Yes, that’s why we use typing, to get better working code more easily. That’s why I use type annotation and enforced checkers in Python. It makes it so much easier and quicker to create good systems of any significance.

    source
• ShroOmeric@lemmy.world ⁨1⁩ ⁨year⁩ ago

  What

  source
• xmunk@sh.itjust.works ⁨1⁩ ⁨year⁩ ago

  I may just be an old country lawyer PHP developer… but don’t most dynamic languages also support static type checking and general analysis at this point?

  source

  • Solemarc@lemmy.world ⁨1⁩ ⁨year⁩ ago

    Yes but no. Modern PHP lets you put types in function signatures and it will then attempt to convert your inputs to those types at runtime.

    JS/TS and Python don’t do this. They have optional type annotations that’s treated as syntactic sugar. You can use static checkers against this but if you get an error like “expected string got int” you can still run the code. It won’t behave any differently because you have annotations.

    source
  • tatterdemalion@programming.dev ⁨1⁩ ⁨year⁩ ago

    Yes if you use type annotations. Languages like Python and Typescript end up resorting to “Any” types a lot of the time, which breaks any kind of theorem proving you might have otherwise benefited from.

    source

    • xmunk@sh.itjust.works ⁨1⁩ ⁨year⁩ ago

      I know Java developers that are addicted to Object. Hit them over the head with an ensmarttening stick and reject their PRs.

      source

      • tzrlk@lemmy.world ⁨1⁩ ⁨year⁩ ago

        Java developers aren’t allowed to not know better by this point. If they think skipping types is somehow ideologically purer, keep hitting with that stick until you hit deckplate.

        source
• tzrlk@lemmy.world ⁨1⁩ ⁨year⁩ ago

  Though even statically-typed languages can need to check types sometimes; parsing runtime data for instance. I can see how you’d do that with pure statics, but it’d just be shifting the work (e.g. if token == QUOTE: proc.call(read_str(bytes, len))). It’d be cool to see a counter example that isn’t unreadable gibberish, however.

  source