From this article's list: "fancy" type systems, functional programming, RISC (!). Formal methods, albeit in specific domains. Security? (I'm not even sure how w

From this article's list: "fancy" type systems, functional programming, RISC (!). Formal methods, albeit in specific domains. Security? (I'm not even sure how we can say whether "security works" or not.) Erlang is a good specific example. Haskell and OCaml are others. (I've seen first hand just how incredibly well OCaml works at Jane Street, even if almost nobody else uses it.) SMT solvers are another cool example. They're used by certain kinds of researchers (including "applied" research like at security companies), but most people haven't even heard of them. At the same time, they let you do some absurd things surprisingly easily that seem intractable. Everything from exhaustively verifying algorithms and invariants to automatically detecting and debugging bugs on the fly to running code backwards. And they make a whole bunch of less absurd but still useful constraint-based problems virtually trivial. Lots of people would benefit from them—if they knew about them and cared. Another great example is the Nix package manager which does package manager magic, but hasn't caught on yet. This is partly a function of its limited ecosystem and documentation, but it does work and I know people using it in production. Hell, for some definition of "widely used", Emacs and VIM fall under this banner. They're somewhat more popular than functional programming and the like, but, in the grand scheme of things, they're a narrow niche among everyday programmers.