On Sat, 17 Jan 2026 00:00:12 GMT, John R Rose <[email protected]> wrote:
> I’m not sure what the intended design rules are here, but for anything > algebraic, fewer axioms are much better than more (murkily related) axioms. > Having many abstract interface points is the same as many axioms — the > witnesses each have their own story for each API point independently. > > The default method approach is very wise, and the body of the default should > be in an implnote in the docs. It amounts to a proof that shows how to (e.g.) > deduce min and max from lower-level axioms. To be precise, for a default method in an interface (unless various special conditions hold*), there should be an impl*Spec* tag (not implNote) that at least documents the general logic and calls to other methods of the interface used in the default method's body. Replicating the full body of the method in the implSpec tag can be acceptable, especially if it is a one-liner, but it is not requited in general. We have multiple examples of this kind of using the JDK APIs, including in javax.lang.model where I'm one of the maintainers. The implSpec tags I included in the changeset to Orderable for it to have default methods follow the general conventions of tag usage for that situation in the JDK. Thanks and HTH. (* The special conditions where an implSpec tag on a default method can be skipped include cases like a default method of a sealed interface where there will be no implementations outside of the shared maintenance domain of the interface.) ------------- PR Review Comment: https://git.openjdk.org/valhalla/pull/1917#discussion_r2700485813
