[bitc-dev] Solver specification?

[Geoffrey Irving]

On Sun, Jan 11, 2009 at 8:58 PM, Tim Sweeney <Tim.Sweeney at epicgames.com> 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