• deegeese@sopuli.xyz
    link
    fedilink
    arrow-up
    31
    arrow-down
    5
    ·
    1 year ago

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

    • tatterdemalion@programming.dev
      link
      fedilink
      arrow-up
      22
      arrow-down
      1
      ·
      edit-2
      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
        link
        fedilink
        arrow-up
        14
        arrow-down
        3
        ·
        edit-2
        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
          link
          fedilink
          arrow-up
          25
          ·
          edit-2
          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.ca
        link
        fedilink
        English
        arrow-up
        7
        ·
        edit-2
        1 year ago

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

        • mikidep@lemmy.worldOP
          link
          fedilink
          arrow-up
          1
          ·
          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. ✌🏻

    • sping@lemmy.sdf.org
      link
      fedilink
      English
      arrow-up
      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.