On Sun, Jan 11, 2009 at 8:58 PM, Tim Sweeney <[email protected]> wrote: > 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.
One way to express a middle ground that would be natural to current programmers is to allow more general solvers, but require the compiler to generate warnings (by default at least) if the base solver fails. The specification would guarantee that warning-free code compiles on any conforming compiler, and that any conforming compiler is required to explain how to remove any warnings it provides. The would mimic how people normally work with C++ across several compilers, but with the guarantee that warning-free on one compiler means warning-free on all. Geoffrey _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
