[bitc-dev] Motivation for BitC Revisited
smagi at higherlogics.com
Wed Mar 10 20:09:33 PST 2010
I think the points you raise about type systems and verification are
spot on, and I'd add that the better the type system, the closer you
get to verification for very little additional effort.
To that end I would recommend refinement types as represented in the
Sage compiler I lieu of full proofs for anyone looking for just a bit
more confidence rather than the total correctness of verification.
On 2010-03-10, at 20:05, "Jonathan S. Shapiro" <shap at eros-os.org> wrote:
> Michal stated in another note:
> As I understand it BitC was developed to allow easily prove some
> properties of programs written in the language.
> Since the motivation has evolved, maybe it's time to re-visit it.
> The original goal for BitC was to give us a systems programming
> language with a modern, safe type system and a fully specified
> semantics. We believed that this was essential to let us prove
> properties about the Coyotos kernel. BitC was built to support a
> verification effort, but that wasn't the only objective. We also
> wanted to bring modern type systems to a broader class of
> programming problems.
> When we started work on BitC, I knew very little about type systems
> or verification. In hindsight, I would say that BitC should simplify
> verification a lot, but for a kernel in the very restricted idiom
> style of Coyotos we could have gotten away with C. We didn't
> understand that until very late in the BitC design process. Also, we
> didn't understand why verification wasn't ultimately a useful place
> to go given our objectives.
> For things *above* the kernel I still think you want a safe systems
> language with a precise semantics. Many of the idiom restrictions
> that make Coyotos's use of C tractable for proof cannot be used in,
> say, the Coyotos space bank.
> While BitC was designed from the first with the Coyotos kernel in
> mind, and we described it as a safe systems language, we never
> intended it to be ONLY a systems language. Everything that is safely
> expressible in Java or C# is also expressible in BitC, and many
> things can be expressed more efficiently or with cleaner abstraction
> in BitC.
> Coyotos is a peculiar system. Within the kernel, there is no benefit
> to GC, because every object is reachable from global state. The
> style of most of our applications is event-loop driven with short
> paths. For most of these applications, there is a clear and natural
> point for GC having negligable overhead. For some others, there is a
> clear distinction between init-time allocation and allocation-free
> execution time. The remaining applications are things we would
> characterize as "large and unprincipled", and for these we were not
> greatly concerned about GC impact.
> Given this combination, we hoped to exploit the "law of the excluded
> middle" in BitC: we elected not to consider applications where GC
> would be a significant impediment. We briefly discussed a manual
> storage strategy in which the "type" of a freed object remained
> unchanged. This is feasible and safe, but the safety contract is a
> bit strange. It can clearly be done, but we saw no reason to hurry.
> Looking back, I would say that most of those assumptions and
> objectives still make sense with one exception: verification.
> We originally chose to go after verification of our kernel for two
> reasons: (1) it was an appropriately high research challenge that we
> thought we could hit, and (2) we wanted to automate more of the
> assurance process.
> With the benefit of greater experience, I would now say that the
> overwhelming majority of the benefit of verification comes from the
> in-going rigor rather than the success of verification. That is:
> it's more important to formally state the objective and the shape of
> the solution than it is to show that you met the objective. It is
> very important to have something that keeps you honest, but a
> sufficiently rich type system can accomplish an awful lot of that.
> At the end of the day, assurance isn't about correctness. It's about
> confidence. That's partly about getting your problem and your
> solution stated right, but it's just as much about being able to
> explain those statements to others. And here we run into the problem
> with formal verification: it's incomprehensible to the auditor. Type
> systems are clearer and more easily explained. They also offer a
> more continuous range of expressiveness than proof systems.
> Today I think that the verification goals remain interesting deep
> research goals, but I'm not in the research business at the moment.
> My near-term goals, as you are seeing in the series of BitC 0.20
> notes, are fairly pragmatic. I do keep circling back to the notion
> of hybrid dependent type, but with great hesitation. ATS is a
> terrific example of the problem: it's incomprehensible. Tim
> Sweeney's work isn't yet visible to the outside world (so far as I
> know). I do think that selective use of dependent type has some real
> value, and maybe that's something to think about once we basically
> have a working language.
> bitc-dev mailing list
> bitc-dev at coyotos.org
More information about the bitc-dev