I agree that in any future language aimed at dependent-typed programming and proof-carrying code (in the proofs-as-programs sense), a program accepted by a developer's compiler must be deterministically accepted by all users.
There are two solutions: 1. As Mark suggests, the solver emits a program and a proof which all users can use to verify it. This allows compilers to implement solvers with different behavior. This approach is unfortunate for developers, who can't necessarily share successfully-compilable code across different compilers for the same base language, but that's not a deal-breaker; for example C++ code isn't fully portable across compilers. 2. As Jonathan noted, the solver is fully specified and operates deterministically. This isn't necessarily hard. For example, the solver could be specified precisely in the language definition, and compilers would only be allowed to differ in optimization. -Tim ________________________________________ From: [email protected] [[email protected]] On Behalf Of Mark Miller [[email protected]] Sent: Sunday, January 11, 2009 4:39 PM To: Discussions about the BitC language Subject: Re: [bitc-dev] Solver specification? 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 _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
