Classic HN: “BitC isn't going to work in its current form” (2012)

This is an experiment in submitting "classic" threads. We already have a culture of periodically resubmitting old stories, but in this case, I think that the combination of the old thread and the story is what is so interesting.

The original submission is, as far as I can tell, the only post-mortem on BitC, which was a research effort for a robust systems programming language. See https://en.wikipedia.org/wiki/BitC for more. The ensuing HN thread has even more insight, as other language designers talk about their own experiences in trying to make a better systems language. Particularly interesting is the comment from pcwalton, talking about similar difficulties with the beginning days of Rust, and how they were overcoming them.

It's interesting looking back on how this compared to the lessons learned by Rust in the lead up to 1.0.

Issues in which Rust observed the same problems and changed course to fixed them:

- Compilation model: Rust originally wanted to do a static compilation model, like BitC, but it eventually went with a hybrid model that leans toward link-time optimization.

- Compiler-Abstracted Representations vs. Optimization: Again, Rust wanted to abstract representations from the compiler, but eventually it just went to a model in which the representations aren't hidden from the compiler.

- Insufficiency of the Type System: Rust also had by-ref parameters only, but as that was insufficient it eventually grew the lifetime system (as well as the subtyping needed to make it usable).

Issues in which Rust persevered anyway:

- Inheritance and Encapsulation: Rust went with interfaces and unified them with the typeclass system.

- Instance Coherence and Operator Overloading: Rust went with a Haskell-like approach to instance coherence. It is sometimes annoying, but it's rarely an insurmountable problem in practice, and Rust is a lot more flexible than most other non-C++, non-D languages here.

SPARK is the only one still going strong in verifiable, systems, programming space. I had hopes for ATS and BitC. There's Rust tie-ins but it's not a verifiable language. There is ongoing work to produce necessary models to make it one but it's quite complex. It's fine, though, as languages like it, Go, and Wirth's were really about raising the baseline safety/security of average code. Way better goal. Whereas, the verifiable languages are about making the highest level of assurance easier even if one must sacrifice some benefits of popular, complex languages.

So, we have SPARK. After much work, C can be subsetted with HOL and AutoCorres. Not really designed for it, though. So, we just have one proper for imperative with another made to work with monumental effort.

Far as functional, we have quite a few options that are prototypes with some production use. Haskell & HOL used with seL4 plus plenty others. Tolmach et al did Habit system language based on Haskell but I think it's on pause. ATS seemed quite practical but hadn't heard anything on it recently. COGENT is a new one for verified, functional, systems language that compiles to C with IIRC certified translation. The ML's have many practical implementations and were designed for theorem proving. CakeML latest in that. PreScheme was verified with VLISP and could be rebooted. There's also model-driven and DSL approach from Hinjtens at iMatix, CertiKOS with DeepSpec team, and Ivory at Galois.

So, this is what we're at since BitC folded. Anyone know of any work I missed with at least one deployment of low-level, OS-style code with realistic, verification capability?