Daniel Weise has gotten Microsoft’s Office group to use code annotations and domain specific checkers to catch bugs. His buffer overrun detector uses a dependent type system based on those annotations to turn buffer overruns into type errors.