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
