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. Therefore I don't expect a prover built into a compiler to do very much (prove that some code is dead so it can be removed, perhaps prove that trivial subranges are not breached so run-time checks can be omitted, 'proving' that a routine is called once so it can be inlined without cost, stuff like that, maybe some clever stuff, but not much). * How much proving should your compiler do unaided? What do you realistically expect? * How much should be left to an external prover driven by a programmer? * 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? * 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? Lots? A few trivial assertions judiciously placed or quite a bit? * Indeed, what is quality code - if I'm given the tools to write fast code (by using int32 instead of UnboundedInt, amongst others) and it runs fast, is that good code? Or is it good only if it's been formally verified to be runtime-safe? The answer is it depends on the requirements, so the issue of proving stuff, or not, is not a technical decision (this is not a well-made point, sorry). * 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? * I'm assuming verification is the key to good code quality, not just correct code - is this a fair assumption? 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). Then there's the human stuff * What is the skill level needed of a human to verify a program? (quite high in my painful experience...) I have always wondered if the external verifier was the key to the language, rather than the compiler. >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). jan _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
