Scrap Your Boilerplate

12 lines of Agda code is verified red-black tree insertion.
12 lines of Java code would be a class declaration with some getters/setters

>>8
You'll be able to redefine getField() to anything else then, like y + z.length, and code will still work.