release 0.0.0.20 and thoughts
Mon, 21 Aug 1995 19:27:17 -0700 (PDT)
On Thu, 17 Aug 1995 email@example.com wrote:
> Who defines need? The language designer? The code designer? The
> code implmementor? The machine owner? The system guru? The end
> user? One what criteria should this choice be made?
Mathematical proof. More accuarely, mathematical proof defines lack of
need, so the system can run that program in an arena lacking that
The real question is, how do we express this mathematical proof to the
system? There are several ways I can think of:
1) just include a list of claims in the software. The OS will trust them
and run the program accordingly. (real likely, huh?)
2) include the working of the proof with the software along with the
claims. The OS will trust only what it has time to verify OR the OS will
refuse to run the program if some of the 'proofs' are invalid (paranoid).
Of course, either way we have to have a way to work out the proof.
That's going to be the main worry. I suspect the proof will be able to
be _followed_ by the computer without human help, but creating the proof
will (in most cases) require programmer intervention.