I'm not sure what to make of these comments here. What Linus does is a mix of software engineering, project management, people management, and product management. Computer science might be a distant fifth, as is the case with most people in the industry. There's no sense in poking fun at homomorphic encryption for being "hip". It's hip because it's a result that computer scientists have been trying to discover for many years, one with tons of potential applications.

I also have to agree that formal verification is largely an academic endeavor. Static analysis is taking off these days but that's not formal verification in any sense. There are a few projects here and there that are formally verified, and certainly there are tools for formal verification, but I've met precious few people in industry who even know how to use proof assistants. This includes my experience working with aerospace clients. Formally verified components, either hardware or software, tend to be small. The first formally verified kernel, for example, is the seL4 microkernel and verification took from 2006 to 2009. Suffice it to say there are few formally verified kernels floating around.