coop/preempt [was: Re: release 0.0.0.20 and thoughts]

[Patrick Premont]

> > Implementing coop will be incredibly easy.  Implementing proofs will be 
> > dramatically harder, BUT will allow many good things.
> 
> a) (safe coop <=> proofs) /\ (proofs are hard) => (safe coop is hard)
>    q.e.d.
> 
> b) many good things in the far future are worse than some good things now.

But TUNES is a Usefull Not Expedient System.

> > As I understood it, provable programs were one of the main goals of TUNES.
> 
> where did you read that?  you must've gotten that impression from the amount
> of the discussion that topic.  which was too much, imho.

The fact that proofs are an essetial part of TUNES is clearly outlined
on the Web documents (about the HLL). At least one thing requires
proofs, the type system. But proofs are very usefull elsewhere, like
in partial evaluation. Partial evaluation is a very general problem
and making cooperative programs when it's more efficient is one of
it's special case.

I think this whole debate over coop VS preempt multitasking is being
done far too early. We should implement preemptive multitasking and
only once we have the HLL working with a proof system should we
consider adding transparent cooperative multitasking to increase performance
when/if it can. But before that we'll be using the proof system to get
far more important performance increases like proving the type or the
value of something at compile type (partial evaluation time).

Patrick