diff --git a/README.md b/README.md
index 39c5447..4448308 100644
--- a/README.md
+++ b/README.md
@@ -44,21 +44,23 @@ Import attributes have to be made available in several different contexts. This
 
 Here, a key-value syntax is used, with the key `type` used as an example indicating the module type. Such key-value syntax can be used in various different contexts.
 
-The `with` syntax in the `ImportDeclaration` statement uses curly braces, for the following reasons (as discussed in [#5](https://github.com/tc39/proposal-import-attributes/issues/5)):
+The `if` syntax in the `ImportDeclaration` statement uses curly braces, for the following reasons (as discussed in [#5](https://github.com/tc39/proposal-import-attributes/issues/5)):
 - JavaScript developers are already used to the Object literal syntax and since it allows a trailing comma copy/pasting attributes will be easy.
-- Follow-up proposals might specifying new types of import attributes (see [Restriction to "check attributes"](https://github.com/tc39/proposal-import-attributes#restriction-to-check-attributes)) and we will be able to group attributes with different keywords, for instance:
+- Follow-up proposals might specify new types of import attributes (see [Restriction to "check attributes"](https://github.com/tc39/proposal-import-attributes#restriction-to-check-attributes)) and we will be able to group attributes with different keywords, for instance:
 ```js
 import json from "./foo.json" if { type: "json" } with { transformA: "value" };
 ```
 
+The `if` keyword is designed to match the check-only semantics. As shown by the example above, one could imagine a new follow-up proposal that uses `with` for "evaluator" attributes.
+
 ### import statements
 
-The ImportDeclaration would allow any arbitrary attributes after the `with` keyword.
+The ImportDeclaration would allow any arbitrary attributes after the `if` keyword.
 
 For example, the `type` attribute indicates a module type, and can be used to load JSON modules with the following syntax.
 
 ```mjs
-import json from "./foo.json" with { type: "json" };
+import json from "./foo.json" if { type: "json" };
 ```
 
 ### dynamic import()
@@ -66,10 +68,10 @@ import json from "./foo.json" with { type: "json" };
 The `import()` pseudo-function would allow import attributes to be indicated in an options bag in the second argument.
 
 ```js
-import("foo.json", { with: { type: "json" } })
+import("foo.json", { if: { type: "json" } })
 ```
 
-The second parameter to `import()` is an options bag, with the only option currently defined to be `with`: the value here is an object containing the import attributes. There are no other current proposals for entries to put in the options bag, but better safe than sorry with forward-compatibility.
+The second parameter to `import()` is an options bag, with the only option currently defined to be `if`: the value here is an object containing the import attributes. There are no other current proposals for entries to put in the options bag, but better safe than sorry with forward-compatibility.
 
 ### Integration of modules into environments
 
@@ -78,17 +80,17 @@ Host environments (e.g., the Web platform, Node.js) often provide various differ
 #### Worker instantiation
 
 ```js
-new Worker("foo.wasm", { type: "module", with: { type: "webassembly" } });
+new Worker("foo.wasm", { type: "module", if: { type: "webassembly" } });
 ```
 
 Sidebar about WebAssembly module types and the web: it's still uncertain whether importing WebAssembly modules would need to be marked specially, or would be imported just like JavaScript. Further discussion in [#19](https://github.com/littledan/proposal-module-attributes/issues/19).
 
 #### HTML
 
-The idea here would be that each import attribute, preceded by `with`, becomes an HTML attribute which could be used in script tags.
+Although changes to HTML won't be specified by TC39, an idea here would be that each import attribute, preceded by `if`, becomes an HTML attribute which could be used in script tags.
 
 ```html
-<script src="foo.wasm" type="module" withtype="webassembly"></script>
+<script src="foo.wasm" type="module" iftype="webassembly"></script>
 ```
 
 (See the caveat about WebAssembly above.)
@@ -101,13 +103,13 @@ In the context of the [WebAssembly/ESM integration proposal](https://github.com/
 
 ### JSON modules
 
-JSON modules are required to be supported when invoked using the `with { type: "json" }` syntax, with common semantics in all JavaScript implementations for this syntax.
+JSON modules are required to be supported when invoked using the `if { type: "json" }` syntax, with common semantics in all JavaScript implementations for this syntax.
 
 JSON modules' semantics are those of a single default export which is the entire parsed JSON document.
 
 Each JavaScript host is expected to provide a secondary way of checking whether a module is a JSON module. For example, on the Web, the MIME type would be checked to be a JSON MIME type. In "local" desktop/server/embedded environments, the file extension may be checked (possibly after symlinks are followed). The `type: "json"` is indicated at the import site, rather than *only* through that other mechanism in order to prevent the privilege escalation issue noted in the opening section.
 
-Nevertheless, the interpretation of module loads with no attributes remains host/implementation-defined, so it is valid to implement JSON modules without *requiring* `with { type: "json" }`. It's just that `with { type: "json" }` must be supported everywhere. For example, it will be up to Node.js, not TC39, to decide whether import attributes are required or optional for JSON modules.
+Nevertheless, the interpretation of module loads with no attributes remains host/implementation-defined, so it is valid to implement JSON modules without *requiring* `if { type: "json" }`. It's just that `if { type: "json" }` must be supported everywhere. For example, it will be up to Node.js, not TC39, to decide whether import attributes are required or optional for JSON modules.
 
 ### Import attributes
 
@@ -176,7 +178,7 @@ Another option considered and not selected has been to use a single string as th
 We could permit import attributes to have more complex values than simply strings, for example:
 
 ```js
-import value from "module" with attr: { key1: "value1", key2: [1, 2, 3] };
+import value from "module" if attr: { key1: "value1", key2: [1, 2, 3] };
 ```
 
 This would allow import attributes to scale to support a larger variety of metadata.
@@ -201,14 +203,14 @@ import value from "module" as "json";
 import value from "module" with type: "json";
 
 // Current proposal, to settle on before Stage 3
-import value from "module" with { type: "json" };
+import value from "module" if { type: "json" };
 ```
 
 #### Before stage 3
 
 After Stage 2 and before Stage 3, we're open to settling on some less core details, such as:
 
-- Considering alternatives for the `with` keyword ([#3](https://github.com/tc39/proposal-module-attributes/issues/3))
+- Considering alternatives for the `with`/`if` keywords ([#3](https://github.com/tc39/proposal-module-attributes/issues/3))
 
 ```mjs
 import value from "module" when { type: 'json' };
@@ -218,7 +220,7 @@ import value from "module" given { type: 'json' };
 - How dynamic import would accept import attributes: e.g., with or without an extra level of nesting
 
 ```mjs
-import("foo.wasm", { with: { type: "webassembly" } });
+import("foo.wasm", { if: { type: "webassembly" } });
 import("foo.wasm", { type: "webassembly" });  // an alternative
 ```
 
@@ -228,7 +230,7 @@ import("foo.wasm", { type: "webassembly" });  // an alternative
     - For example, in the Web Platform, how import attributes would be enabled when launching a worker (if that is supported in the initial version to be shipped on the Web) or included in a `<script>` tag.
 
 ```mjs
-new Worker("foo.wasm", { type: "module", with: { type: "webassembly" } });
+new Worker("foo.wasm", { type: "module", if: { type: "webassembly" } });
 ```
 
 Standardization here would consist of building consensus not just in TC39 but also in WHATWG HTML as well as the Node.js ESM effort and a general audit of semantic requirements across various host environments ([#10](https://github.com/tc39/proposal-module-attributes/issues/10), [#24](https://github.com/tc39/proposal-module-attributes/issues/24) and [#25](https://github.com/tc39/proposal-module-attributes/issues/25)).
diff --git a/spec.html b/spec.html
index 2de2853..458d107 100644
--- a/spec.html
+++ b/spec.html
@@ -6,7 +6,7 @@
 <pre class=metadata>
   title: Module attributes
   status: proposal
-  stage: 1
+  stage: 2
   location: https://github.com/tc39/proposal-module-attributes
   copyright: false
   contributors: Sven Sauleau, Myles Borins, Daniel Ehrenberg, Daniel Clark
@@ -23,16 +23,16 @@ <h1>Syntax</h1>
     ImportDeclaration :
       `import` ImportClause FromClause `;`
       `import` ModuleSpecifier `;`
-      <ins>`import` ImportClause FromClause WithClause `;`</ins>
-      <ins>`import` ModuleSpecifier WithClause `;`</ins>
-      <ins>`export` ExportFromClause FromClause WithClause `;`</ins>
+      <ins>`import` ImportClause FromClause IfClause `;`</ins>
+      <ins>`import` ModuleSpecifier IfClause `;`</ins>
+      <ins>`export` ExportFromClause FromClause IfClause `;`</ins>
 
-    WithClause :
-      <ins>`with` `{` WithEntries `}` `;`</ins>
+    IfClause :
+      <ins>`if` `{` AttributeEntries `}` `;`</ins>
 
-    WithEntries :
+    AttributeEntries :
       <ins>IdentifierName `:` StringLiteral</ins>
-      <ins>IdentifierName `:` StringLiteral `,` WithEntries</ins>
+      <ins>IdentifierName `:` StringLiteral `,` AttributeEntries</ins>
 
     ImportCall[Yield, Await] :
       `import` `(` AssignmentExpression[+In, ?Yield, ?Await] `,`? `)`
@@ -43,7 +43,7 @@ <h1>Syntax</h1>
 <emu-clause id="sec-semantics">
   <h1>Semantics</h1>
 
-  <emu-note type="editor"><p>Many productions operating on grammar are the same whether or not an |WithClause|/second |ImportCall| parameter is included; the new parameter is ignored. In this section, only the semantically significant changes are included, and the PR to merge into the main specification would fill in the straightforward details.</p></emu-note>
+  <emu-note type="editor"><p>Many productions operating on grammar are the same whether or not an |IfClause|/second |ImportCall| parameter is included; the new parameter is ignored. In this section, only the semantically significant changes are included, and the PR to merge into the main specification would fill in the straightforward details.</p></emu-note>
 
     <emu-clause id="sec-import-calls">
       <h1>Import Calls</h1>
@@ -76,7 +76,7 @@ <h1>Runtime Semantics: Evaluation</h1>
           1. <ins>Let _arg_ be ? GetValue(_argRef_).</ins>
           1. <ins>If _arg_ is *undefined*, let _attributes_ be an empty List.</ins>
           1. <ins>Otherwise,</ins>
-            1. <ins>Let _attributesObj_ be ? Get(_arg_, *"with"*).</ins>
+            1. <ins>Let _attributesObj_ be ? Get(_arg_, *"if"*).</ins>
             1. <ins>Let _attributes_ be a new empty List.</ins>
             1. <ins>Let _keys_ be EnumerableOwnPropertyNames(_attributesObj_, ~key~).</ins>
             1. <ins>IfAbruptRejectPromise(_keys_, _promiseCapability_).</ins>
@@ -141,7 +141,7 @@ <h1>Runtime Semantics: HostResolveImportedModule ( _referencingScriptOrModule_,
         </emu-note>
 
         <emu-note type=editor>
-          <p>The above text implies that hosts *must* support JSON modules imported with `type: "json"` (if it completes normally), but it doesn't prohibit hosts from supporting JSON modules imported with no type specified. Some environments (for example, web browsers) are expected to require `with type: "json"`, and environments which want to restrict themselves to a compatible subset would do so as well.</p>
+          <p>The above text implies that hosts *must* support JSON modules imported with `type: "json"` (if it completes normally), but it doesn't prohibit hosts from supporting JSON modules imported with no type specified. Some environments (for example, web browsers) are expected to require `if { type: "json" }`, and environments which want to restrict themselves to a compatible subset would do so as well.</p>
         </emu-note>
       </emu-clause>
 
@@ -362,33 +362,33 @@ <h1>ParseJSONModule ( _source_ )</h1>
     </emu-alg>
   </emu-clause>
 
-  <emu-clause id="sec-with-clause-early-errors">
+  <emu-clause id="sec-if-clause-early-errors">
     <h1>Static Semantics: Early Errors</h1>
-    <emu-grammar>WithClause : `with` WithEntries</emu-grammar>
+    <emu-grammar>IfClause : `if` AttributeEntries</emu-grammar>
     <ul>
-      <li>It is a Syntax Error if WithClauseToAttributes of |WithClause| has two entries _a_ and _b_ such that _a_.[[Key]] is _b_.[[Key]].</li>
+      <li>It is a Syntax Error if IfClauseToAttributes of |IfClause| has two entries _a_ and _b_ such that _a_.[[Key]] is _b_.[[Key]].</li>
     </ul>
   </emu-clause>
 
-  <emu-clause id="sec-with-clause-to-object" aoid="WithClauseToAttributes">
-    <h1>Runtime Semantics: WithClauseToAttributes</h1>
-    <emu-grammar>WithClause : `with` WithEntries</emu-grammar>
+  <emu-clause id="sec-if-clause-to-object" aoid="IfClauseToAttributes">
+    <h1>Runtime Semantics: IfClauseToAttributes</h1>
+    <emu-grammar>IfClause : `if` AttributeEntries</emu-grammar>
     <emu-alg>
-      1. Let _attributes_ be WithEntriesToAttributes of |WithEntries|.
+      1. Let _attributes_ be IfEntriesToAttributes of |AttributeEntries|.
       1. Sort _attributes_ by the code point order of the [[Key]] of each entry.  NOTE: This sorting is observable only in that hosts are prohibited from distinguishing among attributes by the order they occur in.
       1. Return _attributes_.
     </emu-alg>
 
-    <emu-grammar> WithEntries : IdentifierName `:` StringLiteral </emu-grammar>
+    <emu-grammar> AttributeEntries : IdentifierName `:` StringLiteral </emu-grammar>
     <emu-alg>
       1. Let _entry_ be a Record { [[Key]]: StringValue of |IdentifierName|, [[Value]]: StringValue of |StringLiteral| }.
       1. Return a new List containing the single element, _entry_.
     </emu-alg>
 
-    <emu-grammar> WithEntries : IdentifierName `:` StringLiteral `,` WithEntries </emu-grammar>
+    <emu-grammar> AttributeEntries : IdentifierName `:` StringLiteral `,` AttributeEntries </emu-grammar>
     <emu-alg>
       1. Let _entry_ be a Record { [[Key]]: StringValue of |IdentifierName|, [[Value]]: StringValue of |StringLiteral| }.
-      1. Let _rest_ be WithEntriesToAttributes of |WithEntries|.
+      1. Let _rest_ be IfEntriesToAttributes of |AttributeEntries|.
       1. Return a new List containing _entry_ followed by the entries of _rest_.
     </emu-alg>
   </emu-clause>
@@ -577,10 +577,10 @@ <h1>Static Semantics: ModuleRequests</h1>
           1. <ins>Let _specifier_ be StringValue of the |StringLiteral| contained in |FromClause|.</ins>
           1. <ins>Return a ModuleRequest Record { [[Specifer]]: _specifier_, [[Attributes]]: an empty List }.</ins>
         </emu-alg>
-        <emu-grammar>ImportDeclaration : `import` ImportClause FromClause WithClause `;`</emu-grammar>
+        <emu-grammar>ImportDeclaration : `import` ImportClause FromClause IfClause `;`</emu-grammar>
         <emu-alg>
           1. <ins>Let _specifier_ be StringValue of the |StringLiteral| contained in |FromClause|.</ins>
-          1. <ins>Let _attributes_ be WithClauseToAttributes of |WithClause|.</ins>
+          1. <ins>Let _attributes_ be IfClauseToAttributes of |IfClause|.</ins>
           1. <ins>Return a ModuleRequest Record { [[Specifer]]: _specifier_, [[Attributes]]: _attributes_ }.</ins>
         </emu-alg>
         <emu-grammar>Module : [empty]</emu-grammar>
@@ -612,11 +612,11 @@ <h1>Static Semantics: ModuleRequests</h1>
           1. <ins>Return a ModuleRequest Record { [[Specifer]]: _specifier_, [[Attributes]]: an empty List }.</ins>
         </emu-alg>
         <emu-grammar>
-          ExportDeclaration : `export` ExportFromClause FromClause WithClause `;`
+          ExportDeclaration : `export` ExportFromClause FromClause IfClause `;`
         </emu-grammar>
         <emu-alg>
           1. <ins>Let _specifier_ be StringValue of the |StringLiteral| contained in |FromClause|.</ins>
-          1. <ins>Let _attributes_ be WithClauseToObject of |WithClause|.</ins>
+          1. <ins>Let _attributes_ be IfClauseToObject of |IfClause|.</ins>
           1. <ins>Return a ModuleRequest Record { [[Specifer]]: _specifier_, [[Attributes]]: _attributes_ }.</ins>
         </emu-alg>
         <emu-grammar>