4 ms·

Congratulations, OK Labs solved the halting problem: http://www.ibm.com/developerworks/rational/library/nov05/marasco/index.html http://www.ibm.com/developerwor

Congratulations, OK Labs solved the halting problem: http://www.ibm.com/developerworks/rational/library/nov05/marasco/index.html http://www.ibm.com/developerworks/rational/library/nov05/mar...

ac 16y ago
No they didn't. And proving correctness of software isn't the same as solving the halting problem. You're confusing formal verification and static analysis (that doesn't mean that the latter doesn't work). Please, google Curry-Howard Isomorphism and Rice's Theorem, will ya?
shasta 16y ago
"Can a program ever be proven correct? No. There may be some very trivial toy programs that under very special conditions can be proven "correct" -- that is, we can mathematically prove that they will never give an incorrect result.5 In the real world of programs, however, the answer is no. At first, one is tempted to believe that it is simply a question of combinatorics. That is, if one considers all the permutations of all the paths through any non-trivial piece of software, one quickly comes to the conclusion that exhaustively testing any piece of software is an impossible task. This is analogous to the NP Complete problem. But, in fact, it is even worse than that. It turns out that proving programs correct is equivalent to solving the Halting Problem. And we know from Turing's work that that is an impossible task." Your link is filled with nonsense, including the conclusion you took away from it here. We're talking about proving properties of a particular program here, not an arbitrary one. Please don't link to that in public again. It's a really terrible article.
- allwein 16y ago
  From the article: "Its unique feature is that it has been mathematically proven to operate correctly, enabling it to separate trusted from untrusted software, protecting critical services from a failure or a malicious attack, say the scientists" He may have been basing his reply on this paragraph. If the OS could successfully answer whether any arbitrary program was trusted or untrusted, that this is equivalent to solving the halting problem.
  - shasta 16y ago
    I don't think you're reading that quote right. "Trusted" doesn't mean "trustworthy". What the implementors were probably trying to explain to this poor technical writer is that they have proven that their kernel correctly implements the isolation policies they have formally specified - enabling it to separate (isolate) trusted (kernel level) from untrusted (user level) software.

Congratulations, OK Labs solved the halting problem: http://www.ibm.com/developerworks/rational/library/nov05/marasco/index.html http://www.ibm.com/developerworks/rational/library/nov05/mar...

ac 16y ago

No they didn't. And proving correctness of software isn't the same as solving the halting problem. You're confusing formal verification and static analysis (that doesn't mean that the latter doesn't work). Please, google Curry-Howard Isomorphism and Rice's Theorem, will ya?

shasta 16y ago

"Can a program ever be proven correct? No. There may be some very trivial toy programs that under very special conditions can be proven "correct" -- that is, we can mathematically prove that they will never give an incorrect result.5 In the real world of programs, however, the answer is no. At first, one is tempted to believe that it is simply a question of combinatorics. That is, if one considers all the permutations of all the paths through any non-trivial piece of software, one quickly comes to the conclusion that exhaustively testing any piece of software is an impossible task. This is analogous to the NP Complete problem. But, in fact, it is even worse than that. It turns out that proving programs correct is equivalent to solving the Halting Problem. And we know from Turing's work that that is an impossible task." Your link is filled with nonsense, including the conclusion you took away from it here. We're talking about proving properties of a particular program here, not an arbitrary one. Please don't link to that in public again. It's a really terrible article.

allwein 16y ago
From the article: "Its unique feature is that it has been mathematically proven to operate correctly, enabling it to separate trusted from untrusted software, protecting critical services from a failure or a malicious attack, say the scientists" He may have been basing his reply on this paragraph. If the OS could successfully answer whether any arbitrary program was trusted or untrusted, that this is equivalent to solving the halting problem.
- shasta 16y ago
  I don't think you're reading that quote right. "Trusted" doesn't mean "trustworthy". What the implementors were probably trying to explain to this poor technical writer is that they have proven that their kernel correctly implements the isolation policies they have formally specified - enabling it to separate (isolate) trusted (kernel level) from untrusted (user level) software.