One small thing: Could the contents of this constructor be lifted into JavaDoc?
The contents of the constructor under this model is surely less burdened by boilerplate, but will still have implementation details that would make for some strange specification reading. So its not quite liftable directly. But the question is still a fair one; how do we better document preconditions, without requiring the user say everything twice?
One possibility, as discussed, is to attach these as their own thing: "require x > 0", which is code that is narrowly targeted enough to lift.
Another is to raise the Preconditions library to more than just a library; let the Javadoc tool have some special treatment for, say, Precondition calls that unconditionally executed in the constructor, where they are boiled down into a documentary form. This has the usual problem of trying to distill intent from imperative code, but perhaps could be sufficiently constrained to work well enough for 95% of preconditions.
Kevin and I have been chatting offline about how some of the accidental problems with Preconditions can be improved with the compiler magic that was described in my recent document on JEP 303. I think that if we can clear some of these accidental hurdles, a standard Precondition library could be more practical, which might pave the way for some of this. (I'll let Kevin explain further.)
Either way, though, I think better support for DBC is an orthogonal feature; I don't think it significantly constrains our ability to deliver a records feature without it.
