On 20 January 2011 13:02, Jonathan S. Shapiro <[email protected]> wrote:
> At the moment, the problem of mixing pure and stateful sub-programs is > standing out as a deep problem. I find that I am caught between conflicting > goals: > > 1. Get an ([artial) advance in the state of the art/practice into the field. > 2. Solve the big problem. > > Of the two, my personal bias is in favor of [1]. > > So here is a (value laden) way of stating the question: > > If BitC, in it's v1 form, gave up on "pure" programming, but leaves the door > open to integration of pure [sub]programming in v2, how many of you would no > longer be interested? > > I personally believe that there is real value in a stateful, strongly-typed > programming language with high performance. It's considerably less than I > initially sought. While I believe the dichotomies can be solved, time is > money, and I'm trying to prioritize attention. I'd still be interested. Given the difficulty of writing a formal spec I'd argue that supporting verification isn't (immediately) a big deal wrt confidence. I think you'd do more to improve the state of the art by building the kind of language you have in mind and then focusing on the issue of a middle ground that you've previously raised on LtU. Lately I've been mulling over the idea that supporting verification per se isn't particularly helpful when you can only achieve at full verification by first writing a specification and then either: 1) Write an implementation and conduct a proof 2) Extract an implementation from the spec Without alternative ways of producing a specification most people would never bridge the chasm between a good type-system and full verification, even if we had a 100% automated prover. Bearing in mind that in many cases I'm not well enough studied to judge the viability of some of these, here are a few things I'd like to see tool support for: 1) Testing libraries for a variety of testing methods, with automated case generation where possible/appropriate 2) Checking for overlapping tests (If I can reduce redundancy I can run more test cases) 3) Automatic verification that a test is meaningful wrt a specification 4) Automatic generation of tests from a specification 5) Specification extraction from (possibly partial) implementations 6) Specification extraction from test suites If BitC had that tooling available there would be numerous options in the middle ground and many additional paths to full verification too. Glen _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
