release 0.0.0.20 and thoughts

[Billy Tanksley]

On Thu, 17 Aug 1995 rdm@tad.micro.umn.edu 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 
resource.

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.

> Raul

-Billy