I have gone for including a solver in the compiler. The solver is (at the moment) a kind of improved Prolog, and theorems to prove, as well as hints can be included with the source.
What is interesting about this approach is that many type system things can be expressed in the logic language without special support in the actual language. Examples of this are type classes and type families, which can be expressed as logic and overloaded functions. Keean. On 2 Jun 2015 18:25, "Jonathan S. Shapiro" <[email protected]> wrote: > The other day, somebody (Keean?) mentioned refinement types, which > prompted me to go look at Liquid Haskell once again. > > I have mixed feelings about things like this. They add some truly > remarkable expressive power to a language - most notably in the area of > proving exception freedom. That's very, very useful, and I'm very much in > favor of that idea. The SPARC/Ada system gets a lot of value out of this. > But i see three issues with them, which are basically the same issues that > I have with dependent types. > > The first issue is that things like refinement types force us into > adopting some form of prover. The problem with this is that we don't really > know how to specify the *behavior* of a prover, so if we add such a > dependency we lose the ability to know whether a given [valid] program > input to the compiler will reliably compile in all compiler > implementations. The best solution I have for this comes in two parts: > > 1. Provide a baseline solver as part of the compiler implementation, whose > presence all implementations can rely on. This guarantees that many > verification conditions can be repeatably discharged in all implementations. > 2. Provide a means (a sub-language) for articulating a proof by hand, such > that the prove can be checked rather than generated by the compiler. This > gets us into questions about proof languages and logics that are more than > I want to bite off at this time. > > The second issue is evolvability. Suppose we implement (e.g.) a certain > SMT solver in BitC v2. Later, in BitC v3, we decide to improve the SMT > solver. How do we make sure that existing programs which rely on the v2 > solver still compile in v3? This is really the solver specification in > disguise, appearing in a new place. > > My final (third) concern is that proof discharge does not always play > nicely with module boundaries. A discharge *here* may require intimate > knowledge of code behavior *there*. Which raises several concerns: > > - We're now engaged in whole-program proof > - The properties we rely on may not be part of the guarantee at the > module interface > - The properties we *need* at the interface tend to grow without > textually reasonable bound. > > This becomes a particular concern as discharge obligations become embedded > in standard libraries. > > If these issues aren't real in practice, then it's definitely worth having > a more serious discussion about all this. It may well be that properties > tied to types are cleaner in these regards than properties more generally. > > So: I really like the idea, but I'm not convinced it should be > incorporated into BitC. A middle position would be to leave a placeholder > syntax for it and do this type of discharge using an external tool for > those programs that need it. > > > shap > > _______________________________________________ > 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
