-----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?

Since you can express any Turing machine in a Turing-complete language,
you have to necessarily deal with Goedel's incompleteness, don't you?

And language side-effects are there, no matter what language, due to the
way it (or its compiler) are implemented.

| 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.

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?

- --
Phillip Gawlowski
Twitter: twitter.com/cynicalryan

~   Why do we drink cow's milk? Who was the first guy who first looked at
a cow and said "I think I'll drink whatever comes out of these things
when I squeeze 'em!"?	  -- Calvin
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.8 (MingW32)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iEYEARECAAYFAkgHJd0ACgkQbtAgaoJTgL9s4QCbBUjq4oK2p5AkQmreI4TmyzTj
DggAnA7rG8GsVcCbyvJBdM8KlHMSqE5E
=RMV1
-----END PGP SIGNATURE-----