On Sun, Jan 11, 2009 at 10:09 AM, Jonathan S. Shapiro <[email protected]> wrote: > 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.
I think an ideal solution to this would have to satisfy the following: 1. Fully portable: any problem that can be compiled with one compiler can be compiled with any other compiler. 2. Fully extensible: there should be no limit on the algorithmic complexity / intelligence of the compiler. As far as I can see, the only way to satisfy both of these is to have a well-defined strict mode, and require any compiler that goes outside strict mode to produce extra annotations that reduce the program to strict mode. I.e., compilers can use any proof generation technique they like, but the proof must be in the form of a new strict-mode program with obviously identical semantics. Another way of stating this is that the "compiler" itself always operates in strict mode, but it is allowable to use a tool that takes a weaker program and fills in the missing annotations. I am not sure whether this is practical or not, since it requires a change in workflow. If the annotation mechanism is optional and even slightly inconvenient, teams of people working with the same good compiler would quickly drop it in favor of using the more expressive language without checking in the annotations alongside. This turns the technical issue into a sociological one. The other problem with this kind of scheme is that is becomes possible to write code which is extremely difficult to modify. I believe that is an inevitable consequence of dependent typing, though, and already occurs even if strict mode is the only possibility. Geoffrey _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
