On Tue, Jun 2, 2015 at 11:24 AM, Jonathan S. Shapiro <s...@eros-os.org> 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.
Another, more experimental option is what I'm trying to do, where the core language only has manual proofs, but also a practical form of proof by reflection that allows libraries to safely add provers and custom checkers. With this approach, the core language can punt on how programmers will actually go about solving proof obligations. And since that's what I've been planning to do, I don't know any good ideas for standardizing provers. > This > gets us into questions about proof languages and logics that are more than I > want to bite off at this time. If you ever decide to bite off the problem of designing a logic and proof language, it's something I know quite a lot about. > 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. Yeah. Basically, I don't know. But in the case of a SMT solver for general purpose stuff, (no language-specific theories) it seems like a better prover would be able to handle all cases of an older prover. That's a guess, based on the hope that general-purpose SMT solvers are sufficiently well-understood. If the guess is right, you might not have to worry about it. I don't know much about automated provers. Are there results about provers that have a known lower bound on the set of problems they can solve? This sort of thing seems like something a lot of people would want, like you, since that lower bound would be something you could require in a language spec. > 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*. My point of view is that there is nothing truly new going on with modularity, just because of logic and proofs. If correctness of A depends on a lot of implementation details of B, then there shouldn't really be an abstraction boundary between A and B. With weak types, you can maybe convince yourself that they can be separated. But if those correctness dependencies were real, then you can't actually modify A and B independently, and expect the combination to still work. In other words, I see the new apparent issues with modularity as just uncovering issues that were really there all along, but not acknowledged by the language. A well-designed system will be modular, no matter how strong the types are. (That can be read either as a strict stance on "well-designed" systems, or an optimistic prediction about systems that would already be considered modular. It's intended mostly as the latter, but I'm willing to fall back to the former.) > Which raises several concerns: > > - We're now engaged in whole-program proof What do you mean? Correctness properties are part of a module interface. Proofs in one module use properties exported by other modules. It seems OK to me. > - The properties we rely on may not be part of the guarantee at the module > interface If you're saying you'd allow a proof to use a property (of code in another module) that isn't part of the module interface, then you _are_ now engaged in whole-program proof, and so you probably shouldn't allow that. I just noticed that--although when programmers talk about modularity, I think we're talking about encapsulation and abstraction--not all modules are opaque. So then maybe all I need to point out is that you can compose a program from translucent modules, and then proofs in one module see the implementation of the other module. But for a large program you'll need abstraction boundaries, so... Maybe what you're getting at is the need for programmers to anticipate the necessary properties for a an abstraction. I see this too as just uncovering a real problem: if you make an abstraction boundary without knowing what properties are really depended upon, then the abstraction was premature. Mathematically speaking, an abstraction should tell you the set of correct implementations. A lot of abstractions in programming are just to allow implementation freedom, and the correctness property is "Works like this naive implementation. (But faster.)". > - The properties we *need* at the interface tend to grow without textually > reasonable bound. Yes. You shouldn't expect to infer them from the code, if that's what you're getting at. Programs with strong properties tend to depend also on libraries of mathematical definitions, which makes writing strong properties feasible. Facts about these definitions get proven, so as to be used in program proofs. Programming environments become proof assistants. > This becomes a particular concern as discharge obligations become embedded > in standard libraries. Hmm. How would that happen? The ways I know of, the obligation would either be solved in the library that causes it, or it gets rediscovered by each user. Either way, you don't end up storing internal obligations in the module interface. > If these issues aren't real in practice, then it's definitely worth having a > more serious discussion about all this. I'm afraid the only real issue is that the maximum expressiveness that refinement types can get in general is squarely at odds with the kind of complete, automatic solution you want for BitC. I don't know about what kinds of special cases of refinement types have complete, automatic solutions. (Sorry if that's what you were asking about all along, and I just wasted our time.) > It may well be that properties tied > to types are cleaner in these regards than properties more generally. I don't know what you mean by "properties tied to types". Aren't all properties tied to the type of object they are properties of? > 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. Maybe it'd be better to let the hypothetical future refinement type system designer design the syntax too. They hypothetically ought to know what they're doing better than us. _______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
