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*.