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. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
