I think his way of doing research is the way computer scientists do research. I.e. instead of taking a very complex programming model (like Java's or Haskell's)

I think his way of doing research is the way computer scientists do research. I.e. instead of taking a very complex programming model (like Java's or Haskell's), most CS researchers invent their own mini languages (that in a lot of cases are simple extensions of lambda calculus or turning machines), these mini languages makes it much easier to reason about specific things. An example: Java's generics were first presented in a paper that added them to a mini-language that only mimicked some properties of Java. That said, his way of working also seems to be very "hackerish", i.e. instead of using "the normal ways", he hacks a model together that show some properties that the conventional and more complex models have a hard time showing. This is basically also how great hackers work, e.g. Paul Graham's Arc (it's very unconventional and simplified - but great at showing the essence of the hacker's ideas). Anyway, great link!