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

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. (from http://www.bitc-lang.org/docs/papers/PLOS2006-shap.html http://www.bitc-lang.org/docs/papers/PLOS2006-shap.html)