in reply to Re: Re: Re: (OT) Where is programming headed?
in thread (OT) Where is programming headed?
couldn't resist.. ;-)
> An axiom system is a series of postulates. An axiom system is
> consistent if it doesn't prove a contraction. That theorem states,
> quite precisely, No consistent finite first order axiom system which
> includes arithmetic can prove its own consistency.
I think we're coming at the problem from opposite directions, so you see an elephant facing left, and I see an elephant facing right.
I agree that no finite set of axioms including arithmetic can generate a system that's simulaneously correct (every statement the basis generates is guaranteed to be true) and complete (the basis is guaranteed to generate every true statement). AFAIK, that doesn't negate either the existence or utility of systems that do generate from finite bases, though.
I never stated a requirement of simultaneous completeness and correctness. I made a quick reference to evoke the concept of formal systems, and in retrospect, I guess I should have said 'Post systems'.
> When using technical terms around people who actually understand
> those terms, it is advisable to give them the usual meaning.
Okay, let's review some vocabulary:
An algorithm is a procedure that solves a problem. The solution it produces must be correct, and the procedure must halt in a finite amount of time.
If an algorithm can solve a problem in finite time, the problem is decidable. If no algorithm can solve the problem in finite time, the problem is undecidable.
A solvable problem is one that can be solved by a Turing machine. A problem that cannot be solved by a Turing machine is unsolvable. Every decidable problem is solvable. Every unsolvable problem is undecidable.
Please note that solvability carries no requirement of finite solution time, the way decidability does. We often use the terms interchangably, but there are times when it's useful to make the distinction between problems that can be solved in infinite time, and problems that can't.
If we say that the halting problem is solvable, it means every program that should halt will, and every program that shouldn't halt won't. That just restates our basic definition of halting, so it must be true. If we say that the halting problem is unsolvable, we admit the possiblity of programs that should halt but don't, and programs that shouldn't halt but do. That directly contradicts our definition of halting, so it must be false. If you reject solutions that take infinite time, you break the definition of halting.
> First of all theorem provers don't ever produce information that
> wasn't a logical consequence of the input. (At least they shouldn't.)
> While we may not have known that output, we do not get out anything
> truly independent of the input.
No arguments there..
> But we do get conclusions that we might not have come up with on our
> own.
Bingo! That's what I'm talking about. The interesting question is how much distance we can put between the specification and the product.
There's a qualitative difference between a program that can extrapolate code from a minimal basis, and a Microsoft wizard. The first explores an infinite generative system, and the second walks through a finite data structure that somebody else filled and ordered. The first can expand its code base on its own, while the second will always be handcuffed to whoever fills its lookup table. The first will produce code that's correct within the limits of its basis and generative capacity, while the second is is subject to all the size -v- implicit bug problems that plague any large body of code.
> Now you seem to be a great fan of the idea that someone somewhere
> will reduce this down to a few axioms. I rather strongly doubt this.
So do I. I just think it's a significant and interesting question.. as opposed to the brain-starved dribblings of a poser who should know better than to try and cut heads with his betters. ;-)
> This is a problem which is going to have many different solutions.
> The trick isn't in making up the missing bits of the specification,
> it is doing it in a way that comes up with answers the human thinks
> are reasonable. And there isn't a simple right answer to that.
And that's why I think we'll always need programmers, no matter how much of the specification can be generated by a program. ;-)
mike
.
|
|---|
| Replies are listed 'Best First'. | |
|---|---|
|
Re (tilly) 4: Re-spect!: (OT) Where is programming headed?
by tilly (Archbishop) on Dec 17, 2001 at 05:15 UTC | |
by mstone (Deacon) on Dec 18, 2001 at 04:52 UTC | |
by tilly (Archbishop) on Dec 18, 2001 at 05:57 UTC |