Learnt today that Checker (for Java) provides pluggable type systems. They've also annotated the whole JDK! Impressive.