I'm a bit miffed as to why MS didn't use F# -- a language from a family of languages designed to implement compilers -- to implement Roslyn. If they had, they could've even gone back later and re-implemented parts of it in F* to guarantee the compiler was bug-free!
If you look at the Roslyn source, I'm not sure this would have worked too well. It looks like a lot of the C# is somewhat unidiomatic as it is (presumably to meet extremely aggressive performance targets), so it's not clear that F# would have provided much benefit. If you're building a compiler that doesn't need to scale to million line codebases, then F#'s a clear winner, but here I'm not so sure.
Please re-read my comment. I didn't suggest implementing the entire Roslyn project in F* , I suggested it might have been better to write it in F#. If that were the case, and the code were written in an idiomatic functional style, it would at least be plausible (although still not easy) to verify parts of the codebase in F*.
