Andrew Wiley: > If that's the purpose, why the hell would they be using C#?
They are now trying again using F* (derived by F#, that is a ML-derived functional language), that has a Coq-proved type system that seems a tour the force: http://lambda-the-ultimate.org/node/4318 > Have they proven the entire CLR as well? The project is unrelated to the CLR. But the people working on the Contracts for C# are (they say) slowly adding contracts to the whole CLR. Bye, bearophile
