"> I've always had the impression that MSR (Microsoft Research) was generally doing much more fundamental research than Google."
They definitely are. Just look at all the MS Research labs and projects. I did once to find them all over the place in terms of both categories of tech and fundamental vs general vs narrow. The Duffy posts on Midori with its design/implementation decisions show how unconventional they can be even when just trying to build a robust, desktop OS whose UI isn't actually radical. Only bad thing is most of best stuff gets turned into patents to stomp on competition. :(
I've met people who worked on Midori and they describe it as the best project they've ever worked on. Used to work in a building with a bunch of old Midori-folks and would ask them about it anytime I heard the word 'Midori'. I don't think it was MSR though.
Personally, I've always been most impressed by the research into formal verification: Z3, Dafny, TLA+, F*, Lean, and many more.
Yeah, their verification tools are incredible. They applied VCC to Hyper-V. The driver tools mostly wiped out blue screens. Got a new one called P language used in USB stack. The methods you mentioned like Dafny got applied in ExpressOS by another team:
Microsoft did it first in VerveOS although Nucleus was ripped off a mainframe OS from the 1970's. VerveOS was impressive where it was one of first safe to the assembly with much less effort than other projects. They also did CoqASM for verified assembly.
A common sentiment on the thread was that Microsoft Research was more akin to Bell Labs.
> I've always had the impression that MSR (Microsoft Research) was generally doing much more fundamental research than Google.
[1] https://news.ycombinator.com/item?id=6919184