An intermediate position is a non-deterministic (an in not fully
specified) solver, which generates a proof, and a deterministic (fully
specified) proof checker. IIUC, this is essentially the PCC
philosophy. The solver is part of one's programming environment, and
different programming environments can have different solvers which
succeed on different programs. However, on any success, any solver
generates a proof which must be acceptable to all checkers. The unit
of transfer is always code + accompanying proof, which should always
be portable among conforming implementations.
Under shared development, code+proof is also the unit checked into
version control. Since the proof isn't actually source, and since the
version control system should never try to merge these, the proof's
versioning should be managed in a different way; perhaps a way that
needs to be invented. The idea may or may not run aground on this
subproblem.
--
Text by me above is hereby placed in the public domain
Cheers,
--MarkM
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
