What you're probably glomming on to is that efforts to push the bounds of what you can prove (higher kinded or dependent types) have had mixed results (mixed in the sense that some people think they're great, others are unconvinced).

So we're in a weird situation where many many people are using a tool, but relatively few are interested in new developments concerning how to use that tool.

I think xchaotic probably meant "in development of production code", and is wrong for two reasons:

1. Compilers are production code, and the research agenda this post describes informs a lot of that code (by way of language design). Unverified compilers still make a lot of use of underlying theory.

2. Correctness proofs and static analyses, which are both deeply related but different from what's being described in this post, are used in production environments every day.