[nickpsecurity]

It's Microsoft Research, specifically, that pulls in most of this great talent. Let's not forget the VMS's people run by Cutler that made the kernel, the Xbox hypervisor, and some other stuff. Add Butler Lampson if we're talking CompSci people. The teams behind Dafny, VerveOS, Ironclad, VCC, etc are way ahead of most language-based safety or formal verification in terms of cost/benefit analysis:

https://en.wikipedia.org/wiki/Butler_Lampson

http://rise4fun.com/

[cwyers]

Of the three parent listed, I think two (Meijer and Hejlsberg) were both DevDiv. Cutler was OS before moving to Xbox of all things, and I think he's at Azure now? It's certainly not only MSR hiring these guys.

[nickpsecurity]

I should've broken up the comment a bit as it looks like I meant all MS Research as you said. I meant to say something along the lines of (1) MS Research is doing a lot of great stuff with some examples and (2) Butler Lampson should've been on the parent's list of top talent at Microsoft. Appreciate you telling me about the mistake, though. :)