David P. Baker

We may be able to use [Docusaurus versioning](https://docusaurus.io/docs/versioning).

Hmm. By "nullable type arguments" do you mean cases like this? ```java @NullMarked interface Foo { void foo(T t); } @NullMarked // test:not-nullness-subtype:String?:String!:Foo#T void test(Foo foo) { foo(null); // not-nullness-subtype...

If this issue is just about changing the non-normative discussion in the spec, then we don't have to debate it here; let's talk about the actual change you want to...

I'll update my last comment to say that if this issue is about changing only the non-normative parts of the spec, then perhaps it shouldn't block the 1.0 release of...

I'm happy to enable it if we think it doesn't require significant setup.

It looks easy enough. I suggest we do that around when we announce 1.0.

I didn't think I had done that, but I guess I did.

As always, I would like to see concrete examples (in conformance test form?) of how the change you're talking about would affect Java types. I'm still otherwise confused. I thought...

OK, I see your argument about the intractibility of a combinatorically large number of worlds. As for your `PerfectlySafe` example, wouldn't JSpecify see that assignment and dereference as cannot-convert-in-some-world, not...

I wonder if we can decide among a few options for moving forward here for 1.0. 1. Maybe **1.0 doesn't need any `@Implies` annotation at all.** Each checker tool has...