If you read the BitC documents, Shapiro mentions that one of the goals of the project was to avoid innovation.
The BitC goal isn't to invent a new language or any new language concepts. It is to integrate existing concepts with advances in prover technology, and reify them in a language that allows us to build stateful low-level systems codes that we can reason about in varying measure using automated tools. The feeling seems to be that everything we are doing is straightforward (read: uninteresting). Would that it were so.
Avoiding innovation in a particular narrow area, while combining others' new idea from other areas in a novel way, is innovation. In fact, it's very rare to see any other form of innovation.
The BitC goal isn't to invent a new language or any new language concepts. It is to integrate existing concepts with advances in prover technology, and reify them in a language that allows us to build stateful low-level systems codes that we can reason about in varying measure using automated tools. The feeling seems to be that everything we are doing is straightforward (read: uninteresting). Would that it were so.
(from http://www.bitc-lang.org/docs/papers/PLOS2006-shap.html)