3 ms·

> but it's mathematically impossible to prove things about computer programs in the general case. there is such thing as verifiable software.

• sebzim4500 4y ago
  True, but you are verifying that the code meets some formal criteria, not that it actually does what you want.
  • riku_iki 4y ago
    formal criteria defines what you want.
    • wizzwizz4 4y ago
      Pray, Mr. Babbage, if you verify the wrong properties, will the right answer come out? Only some software is possible to verify, and there are many properties that it's impossible to verify because the software isn't the only thing that exists in the universe. No amount of mathematical proof on an ideal RAM machine will anticipate rowhammer. And: just because something's theoretically possible, that doesn't mean an AI system would automatically pick up the ability to do it. Verifiable software in practice is still way behind what we currently know to be possible.
      • riku_iki 4y ago
        > No amount of mathematical proof on an ideal RAM machine will anticipate rowhammer. you can infer algorithm failure rate depending on other input factors as an input. Say you found algorithm will fails every 10e15 years of continues run, you can accept such algorithm as reliable.
        • wizzwizz4 4y ago
          > depending on other input factors You're assuming we've solved physics, and that it would be tractable to model all of that. We haven't, and it probably won't be.
          • riku_iki 4y ago
            that's the best approach we can use.