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

>>24

puts logic where it doesn't belong

Who are you to judge that if you can't even understand the principle of encapsulation? Objects are black boxes, they can redistribute logic inside of themselves however the fuck the programmer wants.

You are changing the meaning of a method

I am explicitly not changing the meaning of the method. getArmor() still returns precisely the armor rating effective at precisely the moment of the call.

and expect everything to just magically fall into place

Haha, even the idiot is beginning to appreciate the beauty of the encapsulation principle. Yes, to an undeveloped mind such as yours, good software development techniques such as this must seem like magic. "Any sophisticated technology ..." etc.

all calls to that method just happen to use the new meaning already

They don't happen to use the new meaning, it's that the new "meaning" (new functionality, actually) is the same as the old one - it's just that the underlying representation that has changed! Looks like you're learning something new here.