Re: "Perfect" or "Provable" security both crypto and non-crypto?

From: Douglas A. Gwyn (DAGwyn_at_null.net)
Date: 09/14/04 

Date: Mon, 13 Sep 2004 23:44:01 -0400

Sebastian Gottschalk wrote:
> The problem of finding the invariants of a loop under Hoare calculus is
> equivalent to the halting problem of a turing machine.

For *arbitrary* ("random") programs, sure, but not for
the vast majority of practical programs. And if during
program construction, the correctness checker warned of
a case that it could not readily verify, that would in
itself be an important warning that the code needs to
be examined; something is probably wrong with it.

Relevant Pages

  • Re: Halting tester proof for software engineers without self-reference
    ... unsolvable then an all-knowing mind can not solve it. ... The proof does not say that the Halting problem is unsolvable. ... that such an all-knowing mind is not emulatable by a Turing machine, ... Bob will wait for someone to ask Alice the infallible Turing machine, "Will Bob halt on input XYZ?" ...
    (comp.theory)
  • Re: [PO] Re: Refutation of the Halting Problems Proof (Clarifications Wanted)
    ... > every existing proof of the Undecidability of the Halting Problem. ... "halt analyzer" is a term you need to define, ... TMs don't return results to other TMs. ... "Since returning the result back to the Turing Machine being analyzed is ...
    (comp.theory)
  • Re: [PO] Re: Refutation of the Halting Problems Proof (Clarifications Wanted)
    ... > every existing proof of the Undecidability of the Halting Problem. ... "halt analyzer" is a term you need to define, ... TMs don't return results to other TMs. ... "Since returning the result back to the Turing Machine being analyzed is ...
    (sci.logic)
  • Re: Halting tester proof for software engineers without self-reference
    ... unsolvable then an all-knowing mind can not solve it. ... The proof does not say that the Halting problem is unsolvable. ... that such an all-knowing mind is not emulatable by a Turing machine, ... Bob will wait for someone to ask Alice the infallible Turing machine, "Will Bob halt on input XYZ?" ...
    (comp.theory)
  • Re: Exploiting limitations of Turing machines in Turing tests?
    ... correctly answer _any_ halting problem question. ... You were proposing that there exists some finite set of special Turing ... able to successfully answer _all_ halting problem questions. ... It's a description of some Turing Machine, and some input, with the simple ...
    (comp.ai.philosophy)