4 ms·

Would it help with the bugs in the new and improved ubuntu coreutils?

• Betelbuddy 21d ago
  It will prove the bugs were corrected implemented... :-) And that your mistaken specification of the tax rules in Switzerland, was correctly translated to code, and that your mistaken specification of the process to request a mortgage is mathematically valid...and that your wrong logic about how much centrifugal force your rocket will be able to stand on ascent was mathematically translated to proven correct code running the incorrect logic... Jesus, I cant stand formal methods people...
  • nottorp 21d ago
    I was picking mostly on the rust religion at first. But then I looked things up and ran into https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem …
    • cmrx64 21d ago
      naive applications of this would lead you to believe no knowledge is possible, and that progress is not meaningful when liveness can’t be guaranteed. it’s all rubbish, grandparent is a small mind who can’t figure out how it’s a step up from nothing.
      • svieira 21d ago
        I wouldn't say it's all rubbish - it's very easy for someone new to theorem proving to presume the equivalent of "strong typing will eliminate the possibility of errors", but the more correct understanding is "strong typing will reduce the number of things you have to keep in your head at any one time thus reducing the possibility of errors".
        • nottorp 21d ago
          The thing with ubuntu's rust coreutils is that they, for example, crash when told to recurse because they use actual recursive calls to go into subdirs and run out of stack space if the structure is big enough. What formal correctness proof will detect that?
          • cmrx64 21d ago
            any of the quite many cost-aware logical frameworks. it’s SO. easy. to. do. you fools are just willfully ignorant on how to represent reasoning, despite alleging yourselves to be computer scientists?
  • Jtsummers 21d ago
    I presume you also can't stand people who write software tests for similar reasons? The test is wrong, the code is wrong. The spec is wrong, the code is wrong. What a waste of effort! Just write correct code people! Verification is left as an exercise for the end users. Who cares about them anyways? /s
    • Betelbuddy 21d ago
      Testers are not selling guarantees...
      • Jtsummers 21d ago
        That's exactly what testers are selling though. If they aren't guaranteeing the program is correct (up to what is tested) then what purpose do they serve? Same with formal methods, offering guarantees up to what is proven.
        • Betelbuddy 21d ago
          Oh my my... "Program testing can be used to show the presence of bugs, but never to show their absence" - Edsger Dijkstra
          • Jtsummers 21d ago
            Ah, but you can't stand those formal methods folks, why are you appealing to authority with Edsger Dijkstra?
            • Betelbuddy 21d ago
              You are trying to convince me that because you pressed "A" once on the vending machine and worked, you declare "A" is proven to dispense Coke...
              • Jtsummers 21d ago