diff --git a/docs/property-readonly.md b/docs/property-readonly.md
index d3c80c0..b692e0f 100644
--- a/docs/property-readonly.md
+++ b/docs/property-readonly.md
@@ -27,7 +27,7 @@ Add a modifier to table properties indicating that they are read-only.
 
 This proposal is not about syntax, but it will be useful for examples to have some. Write:
 
-* `get p: T` for a read-only property of type `T`.
+* `read p: T` for a read-only property of type `T`.
 
 For example:
 ```luau
@@ -37,7 +37,7 @@ end
 ```
 has inferred type:
 ```
-f: (t: { p: number, get q: number }) -> ()
+f: (t: { p: number, read q: number }) -> ()
 ```
 indicating that `p` is used read-write but `q` is used read-only.
 
@@ -45,27 +45,27 @@ indicating that `p` is used read-write but `q` is used read-only.
 
 Read-only properties are covariant:
 
-* If `T` is a subtype of `U` then `{ get p: T }` is a subtype of `{ get p: U }`.
+* If `T` is a subtype of `U` then `{ read p: T }` is a subtype of `{ read p: U }`.
 
 Read-write properties are a subtype of read-only properties:
 
-* If `T` is a subtype of `U` then `{ p: T }` is a subtype of `{ get p: U }`.
+* If `T` is a subtype of `U` then `{ p: T }` is a subtype of `{ read p: U }`.
 
 ### Indexers
 
 Indexers can be marked read-only just like properties. In
-particular, this means there are read-only arrays `{get T}`, that are
+particular, this means there are read-only arrays `{read T}`, that are
 covariant, so we have a solution to the "covariant array problem":
 
 ```luau
 local dogs: {Dog}
-function f(a: {get Animal}) ... end
+function f(a: {read Animal}) ... end
 f(dogs)
 ```
 
 It is sound to allow this program, since `f` only needs read access to
-the array, and `{Dog}` is a subtype of `{get Dog}`, which is a subtype
-of `{get Animal}`.  This would not be sound if `f` had write access,
+the array, and `{Dog}` is a subtype of `{read Dog}`, which is a subtype
+of `{read Animal}`.  This would not be sound if `f` had write access,
 for example `function f(a: {Animal}) a[1] = Cat.new() end`.
 
 ### Functions
@@ -80,8 +80,8 @@ function t:m() ... end
 should have type
 ```
 t : {
-  get f : () -> (),
-  get m : (self) -> ()
+  read f : () -> (),
+  read m : (self) -> ()
 }
 ```
 
@@ -107,7 +107,7 @@ since the build method is read-write, so users can update it:
 
 but if we define:
 ```luau
-  type ROFactory<A> = { get build : () -> A }
+  type ROFactory<A> = { read build : () -> A }
 ```
 
 then we do have that `ROFactory<Dog>` is a subtype of `ROFactory<Animal>`
diff --git a/docs/property-writeonly.md b/docs/property-writeonly.md
index defee1d..22e365a 100644
--- a/docs/property-writeonly.md
+++ b/docs/property-writeonly.md
@@ -46,18 +46,18 @@ The reason for these failures is that neither of these is the most
 specific type. It is one which includes that `t.p` is written to, and
 not read from.
 ```luau
-  f : ({ set p: Dog }) -> ()
+  f : ({ write p: Dog }) -> ()
 ```
 
 This allows both example uses of `f` to typecheck. To see that it is more specific than `({ p: Animal }) -> ()`:
 
 * `Dog` is a subtype of `Animal`
-* so (since write-only properties are contravariant) `{ set p: Dog }` is a supertype of `{ set p: Animal }`
-* and (since read-write properties are a subtype of write-only properties)  `{ set p: Animal }` is a supertype of `{ p: Animal }`
-* so (by transitivity)  `{ set p: Dog }` is a supertype of `{ set p: Animal }` is a supertype of `{ p: Animal }`
-* so (since function arguments are contravariant `({ set p: Dog }) -> ()` is a subtype of `({ p: Animal }) -> ()`
+* so (since write-only properties are contravariant) `{ write p: Dog }` is a supertype of `{ write p: Animal }`
+* and (since read-write properties are a subtype of write-only properties)  `{ write p: Animal }` is a supertype of `{ p: Animal }`
+* so (by transitivity)  `{ write p: Dog }` is a supertype of `{ write p: Animal }` is a supertype of `{ p: Animal }`
+* so (since function arguments are contravariant `({ write p: Dog }) -> ()` is a subtype of `({ p: Animal }) -> ()`
 
-and similarly `({ set p: Dog }) -> ()` is a subtype of `({ p: Dog }) -> ()`.
+and similarly `({ write p: Dog }) -> ()` is a subtype of `({ p: Dog }) -> ()`.
 
 Local type inference depends on the existence of most specific (and most general) types,
 so if we want to use it "off the shelf" we will need write-only properties.
@@ -77,7 +77,7 @@ Add a modifier to table properties indicating that they are write-only.
 
 This proposal is not about syntax, but it will be useful for examples to have some. Write:
 
-* `set p: T` for a write-only property of type `T`.
+* `write p: T` for a write-only property of type `T`.
 
 For example:
 ```luau
@@ -87,7 +87,7 @@ end
 ```
 has inferred type:
 ```
-f: (t: { set p: number, get q: number }) -> ()
+f: (t: { write p: number, read q: number }) -> ()
 ```
 indicating that `p` is used write-only but `q` is used read-only.
 
@@ -112,16 +112,16 @@ When declaring a method in a table or class, we should add a read-only property
 
 Write-only properties are contravariant:
 
-* If `T` is a subtype of `U` then `{ set p: U }` is a subtype of `{ set p: T }`.
+* If `T` is a subtype of `U` then `{ write p: U }` is a subtype of `{ write p: T }`.
 
 Read-write properties are a subtype of write-only properties:
 
-* If `T` is a subtype of `U` then `{ p: U }` is a subtype of `{ set p: T }`.
+* If `T` is a subtype of `U` then `{ p: U }` is a subtype of `{ write p: T }`.
 
 ### Indexers
 
 Indexers can be marked write-only just like properties. In
-particular, this means there are write-only arrays `{set T}`, that are
+particular, this means there are write-only arrays `{write T}`, that are
 contravariant. These are sometimes useful, for example:
 
 ```luau
@@ -135,7 +135,7 @@ end
 
 we can give this function the type
 ```
-  move: <a>({a},{set a}) -> ()
+  move: <a>({a},{write a}) -> ()
 ```
 
 and since write-only arrays are contravariant, we can call this with differently-typed
@@ -160,7 +160,7 @@ Once we have read-only properties and write-only properties, type intersection
 gives read-write properties with different types.
 
 ```luau
-  { get p: T } & { set p : U }
+  { read p: T } & { write p : U }
 ```
 
 If we infer such types, we may wish to present them differently, for