Tim's proposal that the runtime should not throw introduces one element that concerns me: the problem of language specification. Here is the issue
In Deputy (which inserts annotation), if the solver cannot discharge a condition, it resolves the requirement by inserting a dynamic check. Deficiencies in the solver manifest as programs with a larger number of inserted annotations. That is: they result in weaker optimization. The language definition does not depend on the behavior of any particular solver. If unsolved constraints are treated as static errors, two implementations of the language using two distinct solvers will not necessarily reject the same programs. Differences may exist in the verification conditions that they are able to discharge, resulting in different programs being rejected. Because the solver determines which programs are rejected, the capabilities of the solver, the rule base over which it operates, and the verification conditions that the front end is obligated to generate become part of the language *specification*. So the complexity "load" of adopting Tim's proposal (on the compiler author) is potentially quite large, but at the moment I'm concerned about specification. So far as I know, no existing dependently-typed language specification provides a rigorous specification of the required behavior of its solver. Does anyone know of any attempt to do this somewhere? Alternatively, does anyone know have thoughts on how one might go about it? A few points seem clear: - The solver's behavior must be deterministic. Acceptance or failure should not be dependent on execution time. At first glance, this appears to rule out higher-order provers. - The compiler must have a "strict" mode, in which any program accepted by any compliant compiler is guaranteed to be accepted by any other compliant compiler. While an implementation should be free to use a better rule base, a better VCG, or a better solver, and it is free to optimize using these, it must retain the capacity to apply the behavior required by the standard and generate errors according to the behavior of the standard solver. - There is a meta-level issue: if we wish to prove the correctness of programs, the prover must be able to simulate the strict solver in order to determine whether the program is well-typed. So: does anyone have any knowledge of how to go about specifying (in the sense of a language reference specification) the required behavior of a solver? If we can't, we may be forced to specify the language in hybrid-typed fashion. Perhaps I should add: This matters because in high confidence software development, it is required that the language being used have a reference specification, and that multiple conforming implementations can exist. This is driven by a desire to avoid the tyranny of a sole supplier, and I think that it is superseded by open source, but the process standards haven't caught up with this aspect of open source yet. Even so, it seems unclean to me that a language specification should be imprecise in this sort of way. FYI, I also created a discussion topic on this at LtU, and I will be tracking discussion in both places. http://lambda-the-ultimate.org/node/3162 shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
