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

>>15
This remains complete nonsense, even if you repeat it FIVE times.

The getter is either trivial or not. If it isn't trivial, there can't ever be a raw field because that would mean putting the logic into every call site, which is beyond retarded. If it is trivial, it's a fundamental property of the object, i.e. any potential getter won't ever change.

The only case where something fundamental enough to be a public field might change is a complete redesign, but preparing for that case is insanity. Your case doesn't exist.