On Thu, Apr 17, 2008 at 12:26 PM, Phillip Gawlowski
<cmdjackryan / googlemail.com> wrote:
> -----BEGIN PGP SIGNED MESSAGE-----
>  Hash: SHA1
>
>  Eivind Eklund wrote:
>
>  |
>  | The Goedel proof is about complete logical systems; in the case of a
>  | computer program, we are working with a system where we have other
>  | formalisms under it that's providing axioms that we don't prove, just
>  | assume.
>
>  But a language that is Turing-complete is a complete logical system, is
>  it not?

No.  A computer language is a different kind of beast; it is not a way
to state truths about things, but a set of rules for mathematical
operations.

The relevance of the incompleteness is in the space of what programs
can exist, and what we can prove about them.

The incompleteness theorem says that there will be statements we can
make about some programs that will be true but that we will not be
able to prove true.

The halting theorem says that, specifically, that there exists
programs that will halt that we cannot prove if halts - under the
assumption of infinite memory.  Under the assumption of finite memory,
we are dealing with a finite state machine, and a proof is *in theory*
possible by enumerating all all the states and which other state
follows that state.

In practice, of course, enumerating all states and the transition from
them very very quickly becomes intractable.

But as far as I can tell, incompleteness does not enter into it; only
practical feasibility.

>  | In the absence of hardware failure (something we of course can't prove
>  | and is a problem in the real world), we can trivially prove halting
>  | for a lot of cases.  E.g, the simple program "halt" halts.  halt if
>  | true halts.  halt if 1 == 1 would generally halt, assuming no
>  | redefinition of ==.  An so on.
>
>  There are logical proofs that P is non-P (details of which are an
>  exercise to the reader since I have misplaced Shaum's Outline of Logic).
>
>  That a state is provable says nothing about the *conditions* that this
>  proof is valid. In a complete system, any proof is valid, so that the
>  proof that halt == true equates to false is a side-effect under the
>  (in-)correct circumstances.

I have no idea what you are trying to say here.  Could you reformulate?

Specifically, the following makes no sense to me:

"In a complete system, any proof is valid" (this seems to depend on
some weird definition of complete system)
"There are logical proofs that P is non-P" (this seems like either an
example of a proof with subtle errors or proof-by-contradiction
proving that a particular statement X is false; ie, if we can prove
P!=P if we assume of X, then we know that X is false.)

>  Now, most applications don't reach this level of complexity, but the
>  level of complexity is there, you usually don't have to care about it.
>
>  Conversely, if every state of a program were provable, the processes
>  like DO-178B wouldn't be necessary, would they?

If we knew we had a perfect spec and could practically prove all the
relevant aspects of  transformation from spec to software/hardware, I
guess we would be able to just say "Prove spec to software" instead of
having any other standard.  Alas, to make software and hardware is a
human endeavor - even assuming we could prove halting properties of
our real world state machines on a perfect computer, this is only a
small part of systems development.

Eivind.