On Thu, Feb 26, 2009 at 8:42 PM, <[email protected]> wrote: > Something happened with my email and I missed this. > > >>On Thu, Feb 26, 2009 at 6:03 PM, Jonathan S. Shapiro <[email protected]> wrote: >>> Range constraints incur a discharge obligation. In the general case, >>> this is an unsolved problem in the literature. >> >>Before I forget to say this... >> >>There is a meta-level problem with constraints. Success at discharging >>them is a function of your prover, and nobody seems to have any way to >>specify what things a prover is *obligated* to prove, nor how to >>satisfy such an obligation. > > The whole term 'prover' is undefined to me here. I don't expect a > general prover to exist that can prove anything very interesting about > a program. That's really my job as a programmer.
But the mechanism you are contemplating really does demand fully automated proof. In practice, about 85% of the proof obligations on vector bounds will be automatically dischargable given a fairly naive checker and a purely local view of the code. The remainder are often quite hard for a human expert even when a fully general proof assistant is available. That's fine, but you introduced the proposition that the compiler should make a very early determination about representation of range-constrained integers based on a proof that it could not discharge. > * How much proving should your compiler do unaided? What do you > realistically expect? I agree that not much is practically obtainable within the compiler. So my practical response to this question is: if you cannot prove it within the compiler, it had better be the case that nothing in the language semantics or the required language pragmatics relies on successful proof. The problem with your range proposal is that it fails this test. > * How much should be left to an external prover driven by a programmer? Anything hard. :-) More generally, anything that isn't deterministically checkable by some reference prover that can be specified by the language standard. Using a prover (internal or external) for optimization is fine. But if the definition of a correct program input relies in any way on a prover, that prover needs to be precisely specifiable. I've been asking in various places how one would go about rigorously specifying a prover. So far, I haven't gotten anyone anywhere in the world to step up and try to answer that question. > * How much does it matter if a compiler does leave a lot of > verification to the programmer? Most BitC work is going to be general > programming, not need-to-be-verified stuff -- am I right? As long as its optimization or application-specific properties, I think that's fine. There has been a side discussion about providing a means to re-incorporate the synthesized proof trail for compile-time checking, but that's relatively straightforward. > * How much tuning-through-verification (ie. prove x means assert(x) can > be removed) need be done before the compiler gets enough to spit out > quality code? If we emit C-as-assembler, then not much, because GCC already does a lot of this. If we want to emit our own code (which we need to do), then a fair bit, but it's not clear how sophisticated a prover and rule base we actually require. > * You've tried to pin down what a prover should be able to prove about > a program, but do you need to? Should proofs be divorced from programs > so that as a new proof arrives, the compiler can be kicked off to > produce better code? Actually, my point has been that this *can't* be pinned down, so nothing in the language definition should rely on a prover to determine what is admissable. At this point I'm repeating myself; sorry. > * I'm assuming verification is the key to good code quality, not just > correct code - is this a fair assumption? Yes, but the richness of the required verificaion conditions for optimizations is pretty modest. Entirely first-order stuff. > Given that BitC can specify > machine word quantities within the language, where is the role of the > verifier (that was my point in the last email, really). Application specific properties, preconditions, postconditions, and the like. >>In consequence, there is no way that a >>language specification can assure that "integer between 5 and 10" as >>an obligation can actually be satisfied. This means that in general we >>lose the ability to specify which programs are valid according to the >>language definition. > > I don't expect these things to be automatically provable for anything > but trivial cases, I expect the human to be involved, and they *can* > prove these things (and if they can't, well, they haven't the skill or > there's a bug). Well, actually, you did (though you did not mean to). You expected the compiler to make a very early binding decision about representations and sizes whose semantic acceptability was predicated on a whole-program proof that the compiler could not perform. shap _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
