5 ms·

It will prove the bugs were corrected implemented... :-) And that your mistaken specification of the tax rules in Switzerland, was correctly translated to code,

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 28d 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 28d 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 28d 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 28d 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 28d 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 28d 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 28d ago
  Testers are not selling guarantees...
  - Jtsummers 28d 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 28d ago
      Oh my my... "Program testing can be used to show the presence of bugs, but never to show their absence" - Edsger Dijkstra
      - Jtsummers 28d ago
        Ah, but you can't stand those formal methods folks, why are you appealing to authority with Edsger Dijkstra?
        Betelbuddy 28d 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 28d ago

nottorp 28d 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 28d 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 28d 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 28d 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 28d 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 28d 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 28d ago
Testers are not selling guarantees...
- Jtsummers 28d 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 28d ago
    Oh my my... "Program testing can be used to show the presence of bugs, but never to show their absence" - Edsger Dijkstra
    - Jtsummers 28d ago
      Ah, but you can't stand those formal methods folks, why are you appealing to authority with Edsger Dijkstra?
      - Betelbuddy 28d 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 28d ago