Patrick Logan comments on my post about the lack of modern compiled languages for optimized performance by pointing to an excellent article by Dan Friedman and asks "Why not take the road less travelled?"
The Friedman article contains a story by Jonathan Sobel where he relates "winning" a class competition for writing the fastest program by using Scheme as the design language, performing correctness preserving transformations on it, and then finally translating the result into C. I've no doubt that you can do this because I've done it myself. I've taught Scheme for almost 20 years and my Ph.D. work and major research forcus for a decade was formal methods. The problem becomes one of scale.
If there were a small core that needed to be optimized, this wouldn't be a bad method. I could have some confidence that we'd end up with something better than we would by simply sitting down and letting people start writing in C. On the other hand, would you be willing to advise someone else to bet their company on this methodology for a large project, especially considering that the people on the project have no training or experience in these techniques? I can't do that in good conscience.
Like it or not, the world "accretes programs as series of patches" in the words of Paul Graham. That means that all the tools and experience are optimized for that activity. The "wins" for alternative programming styles are almost always presented in the small or at best by a team of experts. I know of no case studies that show large projects being done using more formal tools and methods by people who were, beforehand, unfamiliar with the techniques and unbelievers in its efficacy. Evolving to Patrick's better world is a desirable goal, but I'm not willing to bet someone's company on the uncertain, for me, outcome.