• tatterdemalion@programming.dev
      60·
      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.

      • deegeese@sopuli.xyz
        31·
        1 year ago

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

        • tatterdemalion@programming.dev
          22·
          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 dynamic languages are bad. I’m saying they have different trade-offs.

          • deegeese@sopuli.xyz
            14·
            1 year ago

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

            I find most bugs come from missed or misinterpreted requirements.

            • tatterdemalion@programming.dev
              25·
              1 year ago

              I have a feeling you are misunderstanding what is meant by “theorems for free” here. For example, one theorem that is proven by all safe Rust programs is that they don’t have 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. Otherwise the theorem would not be “free” as stated in OP.

          • floofloof@lemmy.caEnglish
            7·
            1 year ago

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

            • mikidep@lemmy.worldOP
              1·
              10 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. ✌🏻

        • sping@lemmy.sdf.orgEnglish
          4·
          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.

      • xmunk@sh.itjust.works
        4·
        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?

        • Solemarc@lemmy.world
          11·
          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.

        • tatterdemalion@programming.dev
          9·
          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.

          • xmunk@sh.itjust.works
            6·
            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.

            • tzrlk@lemmy.world
              7·
              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.

      • tzrlk@lemmy.world
        1·
        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.

  • jasondj@ttrpg.network
    12·
    1 year ago

    I’m sorry, I’m only a novice Python guy. Know enough to get two RESTful APIs to talk to each other and do some network automation or rudimentary Ansible plugins.

    What’s wrong with if isinstance(x, str):?

    • Knusper@feddit.de
      20·
      1 year ago

      Apparently, “Theorems for free!” is a paper that talks about an extensive ability to reason about parts of programs, if you follow some rather basic rules.

      However, lots of popular programming languages throw this ability out the window, because they do not want to enforce those basic rules.
      Most languages, for example, allow for rather uncontrolled side effects and to be able to reason as a programmer, you have to make the assumption that no one else abused side effects.

      The instanceof is rather referring to dynamic typing, though, as e.g. employed by Python and JS, which makes it difficult to make any assumptions at all.

      So, in statically typed languages, when you’re implementing a function, you can declare that a given parameter is a number or a string etc. and the compiler will enforce that for you. In dynamically typed languages, you have to assume that anyone calling your function is using it correctly, which is a difficult assumption to make after a refactoring in a larger codebase.

      All in all, such different levels of rigorosity can be fine, but the larger your codebase grows, the more you do want such rules to be enforced, so you can just ignore the rest of the codebase.

  • mikidep@lemmy.worldOP
    1·
    10 months ago

    Op here back from the dead. This is in fact not a stab at dynamically typed languages, or at least not only: statically typed languages such as Java also support this kind of construct. In fact, one could develop a technically type safe programming language where an instanceof construct has sound semantics.

    What instanceof breaks is something called polymorphic parametricity, i.e. the fact that generic functions don’t know anything specific about the types they are generic over. This is the fundamental condition for what in the community is dubbed “theorems for free”, that is, naturality of generic functions between generic types.