<div dir="ltr"><div dir="ltr">On Thu, Oct 30, 2025 at 9:38 PM Rob Ross <<a href="mailto:rob.ross@gmail.com">rob.ross@gmail.com</a>> wrote:</div><div class="gmail_quote gmail_quote_container"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Contracts, `runtime` and `compile time`...</div></div></blockquote><div><br></div><div>All good thoughts.</div><div><ol><li>Strongly-typed languages like Java are favored for complex programming tasks because of the rich tools they provide to programmers allowing one to prove to oneself that the code's behavior will be correct. This is Java in a nutshell!</li><li>In general, such tools will operate at <i>both</i> compile/build time and runtime - and they should do so in a coherent way.</li></ol></div><div>The observation I'm trying to make in this thread is: Java gives its own tools the ability to operate seamlessly across both domains (compile-time and runtime) but it makes it difficult for the programmer to add their own tools that operate seamlessly across both domains.</div><div><br></div><div><div>Heck, even the compile-only tools are difficult - for evidence of 
this, count how many <span style="font-family:monospace">import com.sun.tools.javac...</span> statements there
 are in the checker framework...</div><div><br>For example, in Java I can say: <span style="font-family:monospace">Foo x = (Foo)y; </span>This will be checked at both compile time (is the compile-time type of y ever assignable to <span style="font-family:monospace">Foo</span>?) and at runtime (<span style="font-family:monospace">CHECKCAST</span>). Moreover it's necessary that it be checked at both compile-time and at runtime because at compile-time we have some, but not all, of the relevant information. Since we want errors to be detected as soon as possible, we detect what we can at compile time and leave the rest to runtime. These two checks are really the same check, just spread across two different domains - they are "coherent".</div></div><br></div><div class="gmail_quote gmail_quote_container">In an ideal world, I should be able to define my own custom type restriction, with both compile-time and runtime components, and have it checked coherently at both compile-time and runtime.</div><div class="gmail_quote gmail_quote_container"><br><div>An experiment I'm working on (very slowly) is to determine how hard it is to create such a tool using what we have today.</div><div><br></div><div>The least clunky plan I've come up with so far is:</div><div><br></div><div>1. Create a new meta-annotation (e.g., <span style="font-family:monospace">@TypeTag</span>) that you would use like this:</div><div><pre class="gmail-language-java" tabindex="0"><code class="gmail-language-java"><span class="gmail-token gmail-annotation gmail-punctuation"><span style="font-family:arial,sans-serif"></span></span>  <span class="gmail-token gmail-comment">/**
   * Annotates declarations of type {@link String} for which
   * the value must be non-null and a valid E.164 phone number.
   */</span>
  <span class="gmail-token gmail-annotation gmail-punctuation">@Target</span><span class="gmail-token gmail-punctuation">(</span><span class="gmail-token gmail-class-name">ElementType</span><span class="gmail-token gmail-punctuation">.</span>TYPE_USE<span class="gmail-token gmail-punctuation">)</span>
<span style="background-color:rgb(255,255,255)">  <span class="gmail-token gmail-annotation gmail-punctuation">@TypeTag</span><span class="gmail-token gmail-punctuation">(</span>appliesTo <span class="gmail-token gmail-operator">=</span> <span class="gmail-token gmail-class-name">String</span><span class="gmail-token gmail-punctuation">.</span><span class="gmail-token gmail-keyword">class</span><span class="gmail-token gmail-punctuation">,</span> validatedBy <span class="gmail-token gmail-operator">=</span> <span class="gmail-token gmail-class-name">PhoneNumberChecker</span><span class="gmail-token gmail-punctuation">.</span><span class="gmail-token gmail-keyword">class</span><span class="gmail-token gmail-punctuation">)</span></span>
  <span class="gmail-token gmail-keyword">public</span> <span class="gmail-token gmail-annotation gmail-punctuation">@interface</span> <span class="gmail-token gmail-class-name">PhoneNumber</span> <span class="gmail-token gmail-punctuation">{</span></code><br><code class="gmail-language-java"><span class="gmail-token gmail-punctuation">  }</span></code></pre></div>2. Create a checker framework plugin extending the Subtyping checker that does the user-defined type restriction stuff at compile time (e.g., <span style="font-family:monospace">@PhoneNumber String x</span>)<br>3. Create a bytecode analyzer that looks for <span style="font-family:monospace">CAST RuntimeInvisibleTypeAnnotations</span> and inserts corresponding runtime checks (e.g. <span style="font-family:monospace">PhoneNumberChecker.check(x)</span>)<br>4. Require both of the above to be included in your build (maybe they could be wrapped into a single maven plug-in?)</div><div class="gmail_quote gmail_quote_container"><br></div><div class="gmail_quote gmail_quote_container"><div>-Archie</div><div><br></div></div><span class="gmail_signature_prefix">-- </span><br><div dir="ltr" class="gmail_signature">Archie L. Cobbs<br></div></div>