<html><body><div dir="ltr">
Hi all, regarding what the Checker Framework and similar tools can do:</div><div dir="ltr"><br></div><div dir="ltr"><blockquote class="gmail_quote" type="cite" style="margin-left:0.8ex;padding-left:1ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204)"><div>WHAT I WANT: To be able to instead say this:<br></div><div><font face="monospace"><br></font></div><div><span style="font-family:monospace"> public void dial(@PhoneNumber String number) {</span><br></div><div><span style="font-family:monospace"> ... // do whatever</span><br></div><div><span style="font-family:monospace"> }</span><br></div><div><br></div><div>AND have the following be true:<br></div><blockquote type="cite" cite="mid:CAL5bRt_h=6yNDYzNTy_2EcxLA5UkYCn+-_dKAXnTFpgzXK1WOA@mail.gmail.com" style="border-left:1px solid var(--quotedTextColor)!important"><div class="gmail_quote gmail_quote_container"><div>At compile time...<br></div><blockquote class="gmail_quote" style="margin-left:0.8ex;padding-left:1ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204)"><div>I get a warning or error if any code tries to invoke <span style="font-family:monospace">dial()</span> with a "plain" String parameter, or assign a plain String to a <a class="gmail_plusreply" id="m_6566702645474090296m_7276368030570384360gmail-plusReplyChip-4" style="font-family:monospace">@PhoneNumber String</a><br></div><div dir="ltr"><div dir="ltr">There is some well-defined, compiler-sanctioned way to validate a phone number, using custom logic I define, so I can assign it to a<span style="font-family:monospace"> @PhoneNumber String </span>without said error/warning. Even if it involves <span style="font-family:monospace">@SuppressWarnings</span>, I'll take it.<br></div></div></blockquote><div>At runtime...<br></div><blockquote class="gmail_quote" style="margin-left:0.8ex;padding-left:1ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204)"><div>No explicit check of the<span style="font-family:monospace"> number </span>parameter is performed by the <span style="font-family:monospace">dial()</span> method (efficiency)<br></div><div dir="ltr"><div dir="ltr">The<span style="font-family:monospace"> dial() </span>method is guaranteed (modulo sneaky tricks) that<span style="font-family:monospace"> number </span><span style="font-family:arial,sans-serif">is </span>always a valid phone number<br></div></div></blockquote></div></blockquote><div>Obviously you can replace<span style="font-family:monospace"> @PhoneNumber </span>with any other assertion. For example:<span style="font-family:monospace"> public void editProfile(@LoggedIn User user) { ... }</span><br></div><div><br></div><div class="gmail_quote gmail_quote_container"><div dir="ltr"><div dir="ltr"><div>Is the above possible using the checker framework? I couldn't figure out how, though that may be due to my own lack of ability.</div></div></div></div></blockquote><br></div><div dir="ltr">This is all mostly possible via the Checker Framework and similar approaches. You wouldn’t need <code style="border:1px solid rgb(206,206,206);background-color:rgb(248,248,248);padding:0px 3px;border-radius:4px">@SuppressWarnings</code> annotations for validation either, due to <a href="https://checkerframework.org/manual/#type-refinement">type refinement</a>. And, for this type of property, where you’re essentially trying to introduce new subtypes of an existing type and then enforce type compatibility at assignments, the implementation effort to write the checker is pretty low. And features like generics would also be handled out of the box.</div><div dir="ltr"><br></div><div dir="ltr">In terms of the “guarantee” that <code style="border:1px solid rgb(206,206,206);background-color:rgb(248,248,248);padding:0px 3px;border-radius:4px">dial</code> always gets a valid phone number, that requires that all code executed at runtime was checked by the checker. If <code style="border:1px solid rgb(206,206,206);background-color:rgb(248,248,248);padding:0px 3px;border-radius:4px">dial</code> might get invoked by unchecked code (e.g., if it’s part of the public API of some library), then some kind of runtime checks are probably still needed inside <code style="border:1px solid rgb(206,206,206);background-color:rgb(248,248,248);padding:0px 3px;border-radius:4px">dial</code>. (I’m assuming that reflection, dynamic creation of classes, etc. count as “sneaky tricks” but those are also potentially problematic.)</div><div dir="ltr"><br></div><div dir="ltr">In terms of the challenges of running the Checker Framework / barriers to adoption: adding the Checker Framework to your build is not too hard; it’s just another annotation processor plus the corresponding flags to enable / configure the checks you want. As implemented the Checker Framework can introduce a significant build-time overhead (potentially 5X or greater), which may be too much to incur on every compile. This is not fundamental; NullAway takes a similar approach and we measured the overhead to be around 10%. But reducing overhead of the Checker Framework itself may require significant work. One can run the Checker Framework in a CI job separate from the normal build, but this delays feedback to the developer.</div><div dir="ltr"><br></div><div dir="ltr">Honestly I think the biggest barrier to adoption is writing the necessary annotations to get the checker to initially pass; for an extant large code base this can be significant work, depending on the property. There is research on inferring these annotations for existing code bases (<a href="https://kelloggm.github.io/martinjkellogg.com/papers/ase2023-camera-ready.pdf">paper 1</a>, <a href="https://manu.sridharan.net/files/FSE23Practical.pdf">paper 2</a>).</div><div dir="ltr"><br></div><div dir="ltr"><div dir="ltr">Best,</div>Manu </div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Oct 14, 2025 at 18:09:46, Brian Goetz <<a href="mailto:brian.goetz@oracle.com">brian.goetz@oracle.com</a>> wrote:<br></div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" type="cite">
<div><div>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</div>
<div>
<font size="4" face="monospace">There's nothing wrong with
annotations being scanned by frameworks. Indeed, the entire point
of annotations is to allow code authors to decorate source
declarations with "structured comments" in a way that is
scrutable, both statically and dynamically, to frameworks and
tooling*. What annotations are _not_ for is to impart semantics
_at the Java language level_. Annotation plumbing is a service
the language and compiler perform for the benefit of libraries and
frameworks, but it recuses itself from being a beneficiary of that
service. <br>
<br>
<br>
(*At this point someone will typically pipe in "But the compiler
is a tool. Ha! I am very clever." But remember, the Java
compiler has no discretion whatsoever about program semantics.
That discretion belongs purely to the language specification.)<br>
</font><br>
<div class="moz-cite-prefix">On 10/14/2025 8:49 PM, Olexandr Rotan
wrote:<br>
</div>
<blockquote type="cite" cite="mid:CAL5bRt_h=6yNDYzNTy_2EcxLA5UkYCn+-_dKAXnTFpgzXK1WOA@mail.gmail.com">
<div dir="ltr">
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">The
next question in this dialog (which I've only had a few
zillion times) is "what about frameworks that use reflection
to drive semantics." But that one kind of answers itself when
you think about it, so I'll just skip ahead now.)</blockquote>
<div><br>
Just out of curiosity, what was the motivation behind the
annotations with runtime retention if they are not expected to
be scanned for by frameworks? Even if talking about things
like aspect-oriented programming, if advice does not alter the
behaviour of the invocation, it will most likely be designed
to produce some side-effect, which is also a semantics change</div>
</div>
<br>
<div class="gmail_quote gmail_quote_container">
<div dir="ltr" class="gmail_attr">On Tue, Oct 14, 2025 at
7:32 PM Brian Goetz <<a href="mailto:brian.goetz@oracle.com" class="moz-txt-link-freetext">brian.goetz@oracle.com</a>>
wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div>
<blockquote type="cite">
<div dir="ltr">
<div dir="ltr">
<div dir="ltr">
<div>WHAT I WANT: To be able to instead say this:</div>
</div>
<div>
<div><span style="font-family:monospace"><br>
</span></div>
<div><span style="font-family:monospace"> public
void dial(@PhoneNumber String number) {</span></div>
<div><span style="font-family:monospace"> ...
// do whatever</span></div>
<div><span style="font-family:monospace"> }</span></div>
<br>
</div>
<div>AND have the following be true:</div>
<div>
<ul>
<li>At compile time...</li>
<ul>
<li>I get a warning or error if any code tries
to invoke <span style="font-family:monospace">dial()</span> with
a "plain" String parameter, or assign a plain
String to a <a class="gmail_plusreply" id="m_6566702645474090296m_7276368030570384360gmail-plusReplyChip-4" style="font-family:monospace">@PhoneNumber String</a></li>
<li>There is some well-defined,
compiler-sanctioned way to validate a phone
number, using custom logic I define, so I can
assign it to a<span style="font-family:monospace"> @PhoneNumber
String </span>without said error/warning.
Even if it involves <span style="font-family:monospace">@SuppressWarnings</span>,
I'll take it.</li>
</ul>
<li>At runtime...</li>
<ul>
<li>No explicit check of the<span style="font-family:monospace"> number </span>parameter
is performed by the <span style="font-family:monospace">dial()</span>
method (efficiency)</li>
<li>The<span style="font-family:monospace">
dial() </span>method is guaranteed (modulo
sneaky tricks) that<span style="font-family:monospace"> number </span><span style="font-family:arial,sans-serif">is </span>always
a valid phone number</li>
</ul>
</ul>
<div>Obviously you can replace<span style="font-family:monospace"> @PhoneNumber </span>with
any other assertion. For example:<span style="font-family:monospace"> public void
editProfile(@LoggedIn User user) { ... }</span></div>
<div><br>
</div>
<div>Is the above possible using the checker
framework? I couldn't figure out how, though that
may be due to my own lack of ability.</div>
</div>
</div>
</div>
</blockquote>
<br>
Yes, but you get no implicit conversion from String to
@PhoneNumber String -- you have to call a method to
explicitly do the conversion:<br>
<br>
@PhoneNumber String validatePhoneNumber(String s) { ...
do the thing ... }<br>
<br>
This is just a function from String -> @PN String, which
just happens to preserve its input after validating it (or
throws if validation fails.)<br>
<br>
A custom checker can validate that you never assign to,
pass, return, or cast a non-PN String when a PN String is
expected, and generate diagnostics accordingly (warnings or
errors, as you like.) <br>
<br>
<blockquote type="cite">
<div dir="ltr">
<div dir="ltr">
<div>
<div>But even if it is possible via checker
framework or otherwise, I don't see this being
done in any widespread fashion, which seems like
pretty strong evidence that it's too hard.</div>
</div>
</div>
</div>
</blockquote>
<br>
It's not that hard, but it _is_ hard to get people to adopt
this stuff. Very few anno-driven type system extensions
have gained any sort of adoption, even if they are useful
and sound. (And interestingly, a corpus search found that
the vast majority of those that are used have to do with
nullity management.) <br>
<br>
Why don't these things get adopted? Well, friction is
definitely a part of it. You have to set up a custom
toolchain configuration. You have to do some work to
satisfy the stricter type system, which is often fussy and
annoying, especially if you are trying to add it to existing
code. You have to program in a dialect, often one that is
underspecified. Libraries you use won't know that dialect,
so at every boundary between your code and library code that
might result in a new PhoneNumber being exchanged, you have
to introduce some extra code or assertion at the boundary.
And to many developers, this sounds like a lot of extra work
to get marginally increased confidence. <br>
<br>
There is similar data to observe in less invasive static
analysis, too. When people first encounter a good static
analysis tool, they get really excited, it finds a bunch of
bugs fairly quickly, and they want to build it into their
methodology. But somewhere along the line, it falls away.
Part of it is the friction (you have to run it in your CI,
and on each developer workstation, with the same
configuration), and part of it is diminishing returns. But
most developers don't feel like they are getting enough for
the effort.<br>
<br>
Of course, the more we can decrease the friction, the lower
the payback has to be to make it worthwhile.<br>
<br>
<blockquote type="cite">
<div dir="ltr">
<div dir="ltr">
<div>But I think it's OK for certain "sticky notes" to
be understood by the compiler, and have the compiler
offer corresponding assistance in verifying them
(which it is already doing - see below). I also
agree that having annotations affect the generated
bytecode ("runtime semantics") is a big step beyond
that, but maybe that's not necessary in this case.</div>
</div>
</div>
</blockquote>
<br>
There are a few "sticky notes" that the "compiler" does in
fact understand, such as @Override or @FunctionalInterface.
(I put "compiler" in quotes because the compiler doesn't get
to have an opinion about anything semantic; that's the
language spec's job.) But these have a deliberately
limited, narrow role: they capture scrutable structural
assertions that require (per language spec!) the compiler to
statically reject some programs that don't conform to the
assertions, but they never have any lingusitic semantics for
correct programs. That is, for a correct program P with
annotations, stripping all annotations out of P MUST produce
a semantically equivalent program. (The next question in
this dialog (which I've only had a few zillion times) is
"what about frameworks that use reflection to drive
semantics." But that one kind of answers itself when you
think about it, so I'll just skip ahead now.)<br>
<br>
<br>
</div>
</blockquote>
</div>
</blockquote>
<br>
</div>
</div>
</blockquote>
</div></body></html>