diff --git a/.github/workflows/prototyping.yml b/.github/workflows/prototyping.yml
index 4a1b8e08..fe458673 100644
--- a/.github/workflows/prototyping.yml
+++ b/.github/workflows/prototyping.yml
@@ -34,6 +34,11 @@ jobs:
       with:
         path: ~/.cabal/store
         key: prototyping-${{ runner.os }}-${{ matrix.agda }}
+    - uses: actions/cache@v2
+      id: luau-ast-cache
+      with:
+        path: ./build
+        key: prototyping-${{ runner.os }}-${{ hashFiles('Ast/**', 'Analysis/**', 'CLI/Ast.cpp', 'CLI/FileUtils.*')}}
     - name: install cabal
       run: sudo apt-get install -y cabal-install
     - name: cabal update
@@ -43,26 +48,35 @@ jobs:
       working-directory: prototyping
       run: |
         cabal install Agda-${{ matrix.agda }}
-        cabal install --lib scientific --package-env .
-        cabal install --lib vector --package-env .
-        cabal install --lib aeson --package-env .
-    - name: check examples
+        cabal install --lib scientific vector aeson --package-env .
+    - name: check targets
       working-directory: prototyping
-      run: ~/.cabal/bin/agda Examples.agda
+      run: |
+        ~/.cabal/bin/agda Examples.agda
+        ~/.cabal/bin/agda Properties.agda
     - name: build executables
       working-directory: prototyping
       run: |
         ~/.cabal/bin/agda --compile PrettyPrinter.agda
         ~/.cabal/bin/agda --compile Interpreter.agda
     - name: cmake configure
-      run: cmake .
+      if: steps.luau-ast-cache.outputs.cache-hit != 'true'
+      run: |
+        mkdir -p build
+        cd build
+        cmake build ../
     - name: cmake build luau-ast
-      run: cmake --build . --target Luau.Ast.CLI
-    - name: run smoketest
+      if: steps.luau-ast-cache.outputs.cache-hit != 'true'
+      run: |
+        cmake --build ./build --target Luau.Ast.CLI
+    - name: run tests
       working-directory: prototyping
       run: |
-        ../luau-ast Examples/SmokeTest.lua | ./PrettyPrinter > Examples/SmokeTestOutput.lua
-        ../luau-ast Examples/SmokeTest.lua | ./Interpreter
-    - name: diff smoketest
-      working-directory: prototyping
-      run: diff Examples/SmokeTest.lua Examples/SmokeTestOutput.lua
+        mkdir test-failures
+        python tests.py -l ../build/luau-ast --write-diff-failures --diff-failure-location test-failures/
+    - uses: actions/upload-artifact@v2
+      if: failure()
+      with:
+        name: test failures
+        path: prototyping/test-failures
+        retention-days: 5
diff --git a/VM/include/lua.h b/VM/include/lua.h
index c5dcef25..5f39cb3d 100644
--- a/VM/include/lua.h
+++ b/VM/include/lua.h
@@ -178,11 +178,11 @@ LUA_API int lua_pushthread(lua_State* L);
 /*
 ** get functions (Lua -> stack)
 */
-LUA_API void lua_gettable(lua_State* L, int idx);
-LUA_API void lua_getfield(lua_State* L, int idx, const char* k);
-LUA_API void lua_rawgetfield(lua_State* L, int idx, const char* k);
-LUA_API void lua_rawget(lua_State* L, int idx);
-LUA_API void lua_rawgeti(lua_State* L, int idx, int n);
+LUA_API int lua_gettable(lua_State* L, int idx);
+LUA_API int lua_getfield(lua_State* L, int idx, const char* k);
+LUA_API int lua_rawgetfield(lua_State* L, int idx, const char* k);
+LUA_API int lua_rawget(lua_State* L, int idx);
+LUA_API int lua_rawgeti(lua_State* L, int idx, int n);
 LUA_API void lua_createtable(lua_State* L, int narr, int nrec);
 
 LUA_API void lua_setreadonly(lua_State* L, int idx, int enabled);
diff --git a/VM/src/lapi.cpp b/VM/src/lapi.cpp
index 29d5f397..39c76e08 100644
--- a/VM/src/lapi.cpp
+++ b/VM/src/lapi.cpp
@@ -659,16 +659,16 @@ int lua_pushthread(lua_State* L)
 ** get functions (Lua -> stack)
 */
 
-void lua_gettable(lua_State* L, int idx)
+int lua_gettable(lua_State* L, int idx)
 {
     luaC_checkthreadsleep(L);
     StkId t = index2addr(L, idx);
     api_checkvalidindex(L, t);
     luaV_gettable(L, t, L->top - 1, L->top - 1);
-    return;
+    return ttype(L->top - 1);
 }
 
-void lua_getfield(lua_State* L, int idx, const char* k)
+int lua_getfield(lua_State* L, int idx, const char* k)
 {
     luaC_checkthreadsleep(L);
     StkId t = index2addr(L, idx);
@@ -677,10 +677,10 @@ void lua_getfield(lua_State* L, int idx, const char* k)
     setsvalue(L, &key, luaS_new(L, k));
     luaV_gettable(L, t, &key, L->top);
     api_incr_top(L);
-    return;
+    return ttype(L->top - 1);
 }
 
-void lua_rawgetfield(lua_State* L, int idx, const char* k)
+int lua_rawgetfield(lua_State* L, int idx, const char* k)
 {
     luaC_checkthreadsleep(L);
     StkId t = index2addr(L, idx);
@@ -689,26 +689,26 @@ void lua_rawgetfield(lua_State* L, int idx, const char* k)
     setsvalue(L, &key, luaS_new(L, k));
     setobj2s(L, L->top, luaH_getstr(hvalue(t), tsvalue(&key)));
     api_incr_top(L);
-    return;
+    return ttype(L->top - 1);
 }
 
-void lua_rawget(lua_State* L, int idx)
+int lua_rawget(lua_State* L, int idx)
 {
     luaC_checkthreadsleep(L);
     StkId t = index2addr(L, idx);
     api_check(L, ttistable(t));
     setobj2s(L, L->top - 1, luaH_get(hvalue(t), L->top - 1));
-    return;
+    return ttype(L->top - 1);
 }
 
-void lua_rawgeti(lua_State* L, int idx, int n)
+int lua_rawgeti(lua_State* L, int idx, int n)
 {
     luaC_checkthreadsleep(L);
     StkId t = index2addr(L, idx);
     api_check(L, ttistable(t));
     setobj2s(L, L->top, luaH_getnum(hvalue(t), n));
     api_incr_top(L);
-    return;
+    return ttype(L->top - 1);
 }
 
 void lua_createtable(lua_State* L, int narray, int nrec)
diff --git a/docs/_pages/grammar.md b/docs/_pages/grammar.md
index 585bac73..ffb1dbf6 100644
--- a/docs/_pages/grammar.md
+++ b/docs/_pages/grammar.md
@@ -68,8 +68,8 @@ SingletonType = STRING | 'true' | 'false'
 
 Type =
     SimpleType ['?'] |
-    SimpleType ['|' Type] |
-    SimpleType ['&' Type]
+    Type ['|' Type] |
+    Type ['&' Type]
 
 GenericTypePackParameter = NAME '...' ['=' (TypePack | VariadicTypePack | GenericTypePack)]
 GenericTypeParameterList = NAME ['=' Type] [',' GenericTypeParameterList] | GenericTypePackParameter {',' GenericTypePackParameter}
diff --git a/docs/_pages/lint.md b/docs/_pages/lint.md
index de4d247e..340d35a2 100644
--- a/docs/_pages/lint.md
+++ b/docs/_pages/lint.md
@@ -317,3 +317,13 @@ The code above can be rewritten as follows to avoid the warning and the associat
 ```lua
 local x = if flag then false else true
 ```
+
+## CommentDirective (26)
+
+Luau uses comments that start from `!` to control certain aspects of analysis, for example setting type checking mode via `--!strict` or disabling individual lints with `--!nolint`. Unknown directives are ignored, for example `--!nostrict` doesn't have any effect on the type checking process as the correct spelling is `--!nonstrict`. This warning flags comment directives that are ignored during processing:
+
+```lua
+--!nostrict
+-- Unknown comment directive 'nostrict'; did you mean 'nonstrict'?"
+```
+```
diff --git a/prototyping/.gitignore b/prototyping/.gitignore
index cca4f464..10edac52 100644
--- a/prototyping/.gitignore
+++ b/prototyping/.gitignore
@@ -2,5 +2,11 @@
 *.agdai
 Main
 MAlonzo
+Examples
 PrettyPrinter
+Interpreter
+Properties
+!Tests/Interpreter
+!Tests/PrettyPrinter
 .ghc.*
+test-failures/
diff --git a/prototyping/Examples/OpSem.agda b/prototyping/Examples/OpSem.agda
index ec8bce7b..c4cfc5e5 100644
--- a/prototyping/Examples/OpSem.agda
+++ b/prototyping/Examples/OpSem.agda
@@ -6,4 +6,3 @@ open import Luau.Heap using (∅)
 
 ex1 : ∅ ⊢ (local (var "x") ← nil ∙ return (var "x") ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ ∅
 ex1 = subst
-
diff --git a/prototyping/Examples/Run.agda b/prototyping/Examples/Run.agda
index 88ca39b6..ddec8e8b 100644
--- a/prototyping/Examples/Run.agda
+++ b/prototyping/Examples/Run.agda
@@ -3,8 +3,9 @@
 module Examples.Run where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
-open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩)
-open import Luau.Value using (nil)
+open import Agda.Builtin.Bool using (true; false)
+open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩; number; binexp; +; <; true; false)
+open import Luau.Value using (nil; number; bool)
 open import Luau.Run using (run; return)
 open import Luau.Heap using (lookup-next; next-emp; lookup-next-emp)
 
@@ -13,3 +14,12 @@ import Agda.Builtin.Equality.Rewrite
 
 ex1 : (run (function "id" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "id" $ nil) ∙ done) ≡ return nil _)
 ex1 = refl
+
+ex2 : (run (function "fn" ⟨ var "x" ⟩ is return (number 123.0) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 123.0) _)
+ex2 = refl
+
+ex3 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (number 1.0) + (number 2.0)) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 3.0) _)
+ex3 = refl
+
+ex4 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (number 1.0) < (number 2.0)) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (bool true) _)
+ex4 = refl
diff --git a/prototyping/FFI/Data/Bool.agda b/prototyping/FFI/Data/Bool.agda
deleted file mode 100644
index 4b04b033..00000000
--- a/prototyping/FFI/Data/Bool.agda
+++ /dev/null
@@ -1,8 +0,0 @@
-module FFI.Data.Bool where
-
-{-# FOREIGN GHC import qualified Data.Bool #-}
-
-data Bool : Set where
-  false : Bool
-  true : Bool
-{-# COMPILE GHC Bool = data Data.Bool.Bool (Data.Bool.False|Data.Bool.True) #-}
diff --git a/prototyping/FFI/Data/Scientific.agda b/prototyping/FFI/Data/Scientific.agda
index 8a5be39e..772d3367 100644
--- a/prototyping/FFI/Data/Scientific.agda
+++ b/prototyping/FFI/Data/Scientific.agda
@@ -1,6 +1,21 @@
 module FFI.Data.Scientific where
 
+open import Agda.Builtin.Float using (Float)
+open import FFI.Data.String using (String)
+open import FFI.Data.HaskellString using (HaskellString; pack; unpack)
+
 {-# FOREIGN GHC import qualified Data.Scientific #-}
+{-# FOREIGN GHC import qualified Text.Show #-}
 
 postulate Scientific : Set
 {-# COMPILE GHC Scientific = type Data.Scientific.Scientific #-}
+
+postulate
+  showHaskell : Scientific → HaskellString
+  toFloat : Scientific → Float
+
+{-# COMPILE GHC showHaskell = \x -> Text.Show.show x #-}
+{-# COMPILE GHC toFloat = \x -> Data.Scientific.toRealFloat x #-}
+
+show : Scientific → String
+show x = pack (showHaskell x)
diff --git a/prototyping/FFI/Data/Vector.agda b/prototyping/FFI/Data/Vector.agda
index 2c5d1925..7d2f5012 100644
--- a/prototyping/FFI/Data/Vector.agda
+++ b/prototyping/FFI/Data/Vector.agda
@@ -3,7 +3,7 @@ module FFI.Data.Vector where
 open import Agda.Builtin.Equality using (_≡_)
 open import Agda.Builtin.Int using (Int; pos; negsuc)
 open import Agda.Builtin.Nat using (Nat)
-open import FFI.Data.Bool using (Bool; false; true)
+open import Agda.Builtin.Bool using (Bool; false; true)
 open import FFI.Data.HaskellInt using (HaskellInt; haskellIntToInt; intToHaskellInt)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
 
diff --git a/prototyping/Interpreter.agda b/prototyping/Interpreter.agda
index 3ec5b8d1..fe311e57 100644
--- a/prototyping/Interpreter.agda
+++ b/prototyping/Interpreter.agda
@@ -36,4 +36,3 @@ runString txt | (Right value) = runJSON value
 
 main : IO ⊤
 main = getContents >>= runString
-
diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda
index 878b8bd0..bd75d9d6 100644
--- a/prototyping/Luau/OpSem.agda
+++ b/prototyping/Luau/OpSem.agda
@@ -1,11 +1,50 @@
 module Luau.OpSem where
 
 open import Agda.Builtin.Equality using (_≡_)
+open import Agda.Builtin.Float using (Float; primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv; primFloatEquality; primFloatLess; primFloatInequality)
+open import Agda.Builtin.Bool using (Bool; true; false)
+open import Utility.Bool using (not; _or_; _and_)
+open import Agda.Builtin.Nat using (_==_)
 open import FFI.Data.Maybe using (just)
 open import Luau.Heap using (Heap; _≡_⊕_↦_; _[_]; function_is_end)
 open import Luau.Substitution using (_[_/_]ᴮ)
-open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg)
-open import Luau.Value using (addr; val)
+open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg; binexp; BinaryOperator; +; -; *; /; <; >; ≡; ≅; ≤; ≥; number)
+open import Luau.Value using (addr; val; number; Value; bool)
+open import Luau.RuntimeType using (RuntimeType; valueType)
+
+evalNumOp : Float → BinaryOperator → Float → Value
+evalNumOp x + y = number (primFloatPlus x y)
+evalNumOp x - y = number (primFloatMinus x y)
+evalNumOp x * y = number (primFloatTimes x y)
+evalNumOp x / y = number (primFloatDiv x y)
+evalNumOp x < y = bool (primFloatLess x y)
+evalNumOp x > y = bool (primFloatLess y x)
+evalNumOp x ≡ y = bool (primFloatEquality x y)
+evalNumOp x ≅ y = bool (primFloatInequality x y)
+evalNumOp x ≤ y = bool ((primFloatLess x y) or (primFloatEquality x y))
+evalNumOp x ≥ y = bool ((primFloatLess y x) or (primFloatEquality x y))
+
+evalEqOp : Value → Value → Value
+evalEqOp Value.nil Value.nil = bool true
+evalEqOp (addr x) (addr y) = bool (x == y)
+evalEqOp (number x) (number y) = bool (primFloatEquality x y)
+evalEqOp (bool true) (bool y) = bool y
+evalEqOp (bool false) (bool y) = bool (not y)
+evalEqOp _ _ = bool false
+
+evalNeqOp : Value → Value → Value
+evalNeqOp Value.nil Value.nil = bool false
+evalNeqOp (addr x) (addr y) = bool (not (x == y))
+evalNeqOp (number x) (number y) = bool (primFloatInequality x y)
+evalNeqOp (bool true) (bool y) = bool (not y)
+evalNeqOp (bool false) (bool y) = bool y
+evalNeqOp _ _ = bool true
+
+coerceToBool : Value → Bool
+coerceToBool Value.nil = false
+coerceToBool (addr x) = true
+coerceToBool (number x) = true
+coerceToBool (bool x) = x
 
 data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set
 data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set
@@ -23,17 +62,23 @@ data _⊢_⟶ᴱ_⊣_  where
     -------------------------------------------
     H ⊢ (function F is B end) ⟶ᴱ (addr a) ⊣ H′
 
-  app : ∀ {H H′ M M′ N} →
+  app₁ : ∀ {H H′ M M′ N} →
   
     H ⊢ M ⟶ᴱ M′ ⊣ H′ →
     -----------------------------
     H ⊢ (M $ N) ⟶ᴱ (M′ $ N) ⊣ H′
 
-  beta : ∀ {H M a F B} →
+  app₂ : ∀ {H H′ V N N′} →
+
+    H ⊢ N ⟶ᴱ N′ ⊣ H′ →
+    -----------------------------
+    H ⊢ (val V $ N) ⟶ᴱ (val V $ N′) ⊣ H′
+
+  beta : ∀ {H a F B V} →
   
     H [ a ] ≡ just(function F is B end) →
-    -----------------------------------------------------
-    H ⊢ (addr a $ M) ⟶ᴱ (block (fun F) is local (arg F) ← M ∙ B end) ⊣ H
+    -----------------------------------------------------------------------------
+    H ⊢ (addr a $ val V) ⟶ᴱ (block (fun F) is (B [ V / name(arg F) ]ᴮ) end) ⊣ H
 
   block : ∀ {H H′ B B′ b} →
  
@@ -51,6 +96,34 @@ data _⊢_⟶ᴱ_⊣_  where
     ---------------------------------
     H ⊢ (block b is done end) ⟶ᴱ nil ⊣ H
   
+  binOpEquality :
+    ∀ {H x y} →
+    ---------------------------------------------------------------------------
+    H ⊢ (binexp (val x) BinaryOperator.≡ (val y)) ⟶ᴱ (val (evalEqOp x y)) ⊣ H
+  
+  binOpInequality :
+    ∀ {H x y} →
+    ----------------------------------------------------------------------------
+    H ⊢ (binexp (val x) BinaryOperator.≅ (val y)) ⟶ᴱ (val (evalNeqOp x y)) ⊣ H
+  
+  binOpNumbers :
+    ∀ {H x op y} →
+    -----------------------------------------------------------------------
+    H ⊢ (binexp (number x) op (number y)) ⟶ᴱ (val (evalNumOp x op y)) ⊣ H
+  
+  binOp₁ :
+    ∀ {H H′ x x′ op y} →
+    H ⊢ x ⟶ᴱ x′ ⊣ H′ →
+    ---------------------------------------------
+    H ⊢ (binexp x op y) ⟶ᴱ (binexp x′ op y) ⊣ H′
+  
+  binOp₂ :
+    ∀ {H H′ x op y y′} →
+    H ⊢ y ⟶ᴱ y′ ⊣ H′ →
+    ---------------------------------------------
+    H ⊢ (binexp x op y) ⟶ᴱ (binexp x op y′) ⊣ H′
+
+  
 data _⊢_⟶ᴮ_⊣_  where
 
   local : ∀ {H H′ x M M′ B} →
@@ -88,5 +161,3 @@ data _⊢_⟶*_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set wher
     H′ ⊢ B′ ⟶* B″ ⊣ H″ →
     ------------------
     H ⊢ B ⟶* B″ ⊣ H″
-
-
diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda
index e514dc9d..b479a72a 100644
--- a/prototyping/Luau/RuntimeError.agda
+++ b/prototyping/Luau/RuntimeError.agda
@@ -3,19 +3,25 @@ module Luau.RuntimeError where
 open import Agda.Builtin.Equality using (_≡_)
 open import Luau.Heap using (Heap; _[_])
 open import FFI.Data.Maybe using (just; nothing)
-open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_)
+open import FFI.Data.String using (String)
+open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_; number; binexp)
+open import Luau.RuntimeType using (RuntimeType; valueType)
+open import Luau.Value using (val)
+open import Properties.Equality using (_≢_)
 
 data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set
 data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set
 
 data RuntimeErrorᴱ H where
-  NilIsNotAFunction : ∀ {M} → RuntimeErrorᴱ H (nil $ M)
+  TypeMismatch : ∀ t v → (t ≢ valueType v) → RuntimeErrorᴱ H (val v)
   UnboundVariable : ∀ x → RuntimeErrorᴱ H (var x)
   SEGV : ∀ a → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (addr a)
-  app : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N)
+  app₁ : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N)
+  app₂ : ∀ {M N} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (M $ N)
   block : ∀ b {B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block b is B end)
+  bin₁ : ∀ {M N op} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (binexp M op N)
+  bin₂ : ∀ {M N op} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (binexp M op N)
 
 data RuntimeErrorᴮ H where
   local : ∀ x {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (local x ← M ∙ B)
   return : ∀ {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (return M ∙ B)
-
diff --git a/prototyping/Luau/RuntimeError/ToString.agda b/prototyping/Luau/RuntimeError/ToString.agda
index e8287157..d5528c8b 100644
--- a/prototyping/Luau/RuntimeError/ToString.agda
+++ b/prototyping/Luau/RuntimeError/ToString.agda
@@ -1,19 +1,27 @@
 module Luau.RuntimeError.ToString where
 
+open import Agda.Builtin.Float using (primShowFloat)
 open import FFI.Data.String using (String; _++_)
-open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; NilIsNotAFunction; UnboundVariable; SEGV; app; block)
+open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; TypeMismatch; UnboundVariable; SEGV; app₁; app₂; block; bin₁; bin₂)
+open import Luau.RuntimeType.ToString using (runtimeTypeToString)
 open import Luau.Addr.ToString using (addrToString)
+open import Luau.Syntax.ToString using (exprToString)
 open import Luau.Var.ToString using (varToString)
-open import Luau.Syntax using (name)
+open import Luau.Value.ToString using (valueToString)
+open import Luau.Syntax using (name; _$_)
 
 errToStringᴱ : ∀ {a H B} → RuntimeErrorᴱ {a} H B → String
 errToStringᴮ : ∀ {a H B} → RuntimeErrorᴮ {a} H B → String
 
-errToStringᴱ NilIsNotAFunction = "nil is not a function"
 errToStringᴱ (UnboundVariable x) = "variable " ++ varToString x ++ " is unbound"
 errToStringᴱ (SEGV a x) = "address " ++ addrToString a ++ " is unallocated"
-errToStringᴱ (app E) = errToStringᴱ E
+errToStringᴱ (app₁ E) = errToStringᴱ E
+errToStringᴱ (app₂ E) = errToStringᴱ E
+errToStringᴱ (bin₁ E) = errToStringᴱ E
+errToStringᴱ (bin₂ E) = errToStringᴱ E
 errToStringᴱ (block b E) = errToStringᴮ E ++ "\n  in call of function " ++ varToString b
+errToStringᴱ (TypeMismatch t v _) = "value " ++ valueToString v ++ " is not a " ++ runtimeTypeToString t
 
 errToStringᴮ (local x E) = errToStringᴱ E ++ "\n  in definition of " ++ varToString (name x) 
 errToStringᴮ (return E) = errToStringᴱ E ++ "\n  in return statement"
+ 
diff --git a/prototyping/Luau/RuntimeType.agda b/prototyping/Luau/RuntimeType.agda
new file mode 100644
index 00000000..375fc540
--- /dev/null
+++ b/prototyping/Luau/RuntimeType.agda
@@ -0,0 +1,15 @@
+module Luau.RuntimeType where
+
+open import Luau.Value using (Value; nil; addr; number; bool)
+
+data RuntimeType : Set where
+  function : RuntimeType
+  number : RuntimeType
+  nil : RuntimeType
+  boolean : RuntimeType
+
+valueType : Value → RuntimeType
+valueType nil = nil
+valueType (addr x) = function
+valueType (number x) = number
+valueType (bool _) = boolean
diff --git a/prototyping/Luau/RuntimeType/ToString.agda b/prototyping/Luau/RuntimeType/ToString.agda
new file mode 100644
index 00000000..dfb7c955
--- /dev/null
+++ b/prototyping/Luau/RuntimeType/ToString.agda
@@ -0,0 +1,10 @@
+module Luau.RuntimeType.ToString where
+
+open import FFI.Data.String using (String)
+open import Luau.RuntimeType using (RuntimeType; function; number; nil; boolean)
+
+runtimeTypeToString : RuntimeType → String
+runtimeTypeToString function = "function"
+runtimeTypeToString number = "number"
+runtimeTypeToString nil = "nil"
+runtimeTypeToString boolean = "boolean"
diff --git a/prototyping/Luau/Substitution.agda b/prototyping/Luau/Substitution.agda
index b956aeae..d909c350 100644
--- a/prototyping/Luau/Substitution.agda
+++ b/prototyping/Luau/Substitution.agda
@@ -1,6 +1,6 @@
 module Luau.Substitution where
 
-open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg)
+open import Luau.Syntax using (Expr; Stat; Block; nil; true; false; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg; number; binexp)
 open import Luau.Value using (Value; val)
 open import Luau.Var using (Var; _≡ⱽ_)
 open import Properties.Dec using (Dec; yes; no)
@@ -11,11 +11,15 @@ var_[_/_]ᴱwhenever_ : ∀ {a P} → Var → Value → Var → (Dec P) → Expr
 _[_/_]ᴮunless_ : ∀ {a P} → Block a → Value → Var → (Dec P) → Block a
 
 nil [ v / x ]ᴱ = nil
+true [ v / x ]ᴱ = true
+false [ v / x ]ᴱ = false
 var y [ v / x ]ᴱ = var y [ v / x ]ᴱwhenever (x ≡ⱽ y)
 addr a [ v / x ]ᴱ = addr a
+(number y) [ v / x ]ᴱ = number y
 (M $ N) [ v / x ]ᴱ = (M [ v / x ]ᴱ) $ (N [ v / x ]ᴱ)
 function F is C end [ v / x ]ᴱ = function F is C [ v / x ]ᴮunless (x ≡ⱽ name(arg F)) end
 block b is C end [ v / x ]ᴱ = block b is C [ v / x ]ᴮ end
+(binexp e₁ op e₂) [ v / x ]ᴱ = binexp (e₁ [ v / x ]ᴱ) op (e₂ [ v / x ]ᴱ)
 
 (function F is C end ∙ B) [ v / x ]ᴮ = function F is (C [ v / x ]ᴮunless (x ≡ⱽ name(arg F))) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ fun F))
 (local y ← M ∙ B) [ v / x ]ᴮ = local y ← (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮunless (x ≡ⱽ name y))
@@ -27,4 +31,3 @@ var y [ v / x ]ᴱwhenever no p = var y
 
 B [ v / x ]ᴮunless yes p = B
 B [ v / x ]ᴮunless no p = B [ v / x ]ᴮ
-
diff --git a/prototyping/Luau/Syntax.agda b/prototyping/Luau/Syntax.agda
index 04970b62..57e59a7e 100644
--- a/prototyping/Luau/Syntax.agda
+++ b/prototyping/Luau/Syntax.agda
@@ -1,6 +1,7 @@
 module Luau.Syntax where
 
 open import Agda.Builtin.Equality using (_≡_)
+open import Agda.Builtin.Float using (Float)
 open import Properties.Dec using (⊥)
 open import Luau.Var using (Var)
 open import Luau.Addr using (Addr)
@@ -32,6 +33,18 @@ arg : ∀ {a} → FunDec a → VarDec a
 arg (f ⟨ x ⟩∈ T) = x
 arg (f ⟨ x ⟩) = x
 
+data BinaryOperator : Set where
+  + : BinaryOperator
+  - : BinaryOperator
+  * : BinaryOperator
+  / : BinaryOperator
+  < : BinaryOperator
+  > : BinaryOperator
+  ≡ : BinaryOperator
+  ≅ : BinaryOperator
+  ≤ : BinaryOperator
+  ≥ : BinaryOperator
+
 data Block (a : Annotated) : Set
 data Stat (a : Annotated) : Set
 data Expr (a : Annotated) : Set
@@ -47,9 +60,12 @@ data Stat a where
 
 data Expr a where
   nil : Expr a
+  true : Expr a
+  false : Expr a
   var : Var → Expr a
   addr : Addr → Expr a
   _$_ : Expr a → Expr a → Expr a
   function_is_end : FunDec a → Block a → Expr a
   block_is_end : Var → Block a → Expr a
-
+  number : Float → Expr a
+  binexp : Expr a → BinaryOperator → Expr a → Expr a
diff --git a/prototyping/Luau/Syntax/FromJSON.agda b/prototyping/Luau/Syntax/FromJSON.agda
index 8ae620bb..330739b9 100644
--- a/prototyping/Luau/Syntax/FromJSON.agda
+++ b/prototyping/Luau/Syntax/FromJSON.agda
@@ -1,14 +1,15 @@
 module Luau.Syntax.FromJSON where
 
-open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec)
+open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; var_∈_; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe; VarDec; number; binexp; BinaryOperator; +; -; *; /; ≡; ≅; <; >; ≤; ≥)
 open import Luau.Type.FromJSON using (typeFromJSON)
 
 open import Agda.Builtin.List using (List; _∷_; [])
+open import Agda.Builtin.Bool using (true; false)
 
 open import FFI.Data.Aeson using (Value; Array; Object; object; array; string; fromString; lookup)
-open import FFI.Data.Bool using (true; false)
 open import FFI.Data.Either using (Either; Left; Right)
 open import FFI.Data.Maybe using (Maybe; nothing; just)
+open import FFI.Data.Scientific using (toFloat)
 open import FFI.Data.String using (String; _++_)
 open import FFI.Data.Vector using (head; tail; null; empty)
 
@@ -19,8 +20,12 @@ lokal = fromString "local"
 list = fromString "list"
 name = fromString "name"
 type = fromString "type"
+value = fromString "value"
 values = fromString "values"
 vars = fromString "vars"
+op = fromString "op"
+left = fromString "left"
+right = fromString "right"
 
 data Lookup : Set where
   _,_ : String → Value → Lookup
@@ -32,6 +37,8 @@ lookupIn (key ∷ keys) obj with lookup (fromString key) obj
 lookupIn (key ∷ keys) obj | nothing = lookupIn keys obj
 lookupIn (key ∷ keys) obj | just value = (key , value)
 
+binOpFromJSON : Value → Either String BinaryOperator
+binOpFromString : String → Either String BinaryOperator
 varDecFromJSON : Value → Either String (VarDec maybe)
 varDecFromObject : Object → Either String (VarDec maybe)
 exprFromJSON : Value → Either String (Expr maybe)
@@ -41,6 +48,21 @@ statFromObject : Object → Either String (Stat maybe)
 blockFromJSON : Value → Either String (Block maybe)
 blockFromArray : Array → Either String (Block maybe)
 
+binOpFromJSON (string s) = binOpFromString s
+binOpFromJSON val = Left "Binary operator not a string"
+
+binOpFromString "Add" = Right +
+binOpFromString "Sub" = Right -
+binOpFromString "Mul" = Right *
+binOpFromString "Div" = Right /
+binOpFromString "CompareEq" = Right ≡
+binOpFromString "CompareNe" = Right ≅
+binOpFromString "CompareLt" = Right <
+binOpFromString "CompareLe" = Right ≤
+binOpFromString "CompareGt" = Right >
+binOpFromString "CompareGe" = Right ≥
+binOpFromString s = Left ("'" ++ s ++ "' is not a valid operator")
+
 varDecFromJSON (object arg) = varDecFromObject arg
 varDecFromJSON val = Left "VarDec not an object"
 
@@ -83,6 +105,24 @@ exprFromObject obj | just (string "AstExprLocal") | just x with varDecFromJSON x
 exprFromObject obj | just (string "AstExprLocal") | just x | Right x′ = Right (var (Luau.Syntax.name x′))
 exprFromObject obj | just (string "AstExprLocal") | just x | Left err = Left err
 exprFromObject obj | just (string "AstExprLocal") | nothing = Left "AstExprLocal missing local"
+exprFromObject obj | just (string "AstExprConstantNumber") with lookup value obj
+exprFromObject obj | just (string "AstExprConstantNumber") | just (FFI.Data.Aeson.Value.number x) = Right (number (toFloat x))
+exprFromObject obj | just (string "AstExprConstantNumber") | just _ = Left "AstExprConstantNumber value is not a number"
+exprFromObject obj | just (string "AstExprConstantNumber") | nothing = Left "AstExprConstantNumber missing value"
+exprFromObject obj | just (string "AstExprConstantBool") with lookup value obj
+exprFromObject obj | just (string "AstExprConstantBool") | just (FFI.Data.Aeson.Value.bool true) = Right Expr.true
+exprFromObject obj | just (string "AstExprConstantBool") | just (FFI.Data.Aeson.Value.bool false) = Right Expr.false
+exprFromObject obj | just (string "AstExprConstantBool") | just _ = Left "AstExprConstantBool value is not a bool"
+exprFromObject obj | just (string "AstExprConstantBool") | nothing = Left "AstExprConstantBool missing value"
+exprFromObject obj | just (string "AstExprBinary") with lookup op obj | lookup left obj | lookup right obj
+exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r with binOpFromJSON o | exprFromJSON l | exprFromJSON r
+exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | Right o′ | Right l′ | Right r′ = Right (binexp l′ o′ r′)
+exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | Left err | _ | _ = Left err
+exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | _ | Left err | _ = Left err
+exprFromObject obj | just (string "AstExprBinary") | just o | just l | just r | _ | _ | Left err = Left err
+exprFromObject obj | just (string "AstExprBinary") | nothing | _ | _ = Left "Missing 'op' in AstExprBinary"
+exprFromObject obj | just (string "AstExprBinary") | _ | nothing | _ = Left "Missing 'left' in AstExprBinary"
+exprFromObject obj | just (string "AstExprBinary") | _ | _ | nothing = Left "Missing 'right' in AstExprBinary"
 exprFromObject obj | just (string ty) = Left ("TODO: Unsupported AstExpr " ++ ty)
 exprFromObject obj | just _ = Left "AstExpr type not a string"
 exprFromObject obj | nothing = Left "AstExpr missing type"
@@ -140,3 +180,4 @@ blockFromArray arr | just value | Left err = Left err
 blockFromArray arr | just value | Right S with blockFromArray(tail arr)
 blockFromArray arr | just value | Right S | Left err = Left (err)
 blockFromArray arr | just value | Right S | Right B  = Right (S ∙ B)
+   
\ No newline at end of file
diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda
index 18d36175..58a784bf 100644
--- a/prototyping/Luau/Syntax/ToString.agda
+++ b/prototyping/Luau/Syntax/ToString.agda
@@ -1,6 +1,7 @@
 module Luau.Syntax.ToString where
 
-open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_)
+open import Agda.Builtin.Float using (primShowFloat)
+open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number; BinaryOperator; +; -; *; /; <; >; ≡; ≅; ≤; ≥; binexp; true; false)
 open import FFI.Data.String using (String; _++_)
 open import Luau.Addr.ToString using (addrToString)
 open import Luau.Type.ToString using (typeToString)
@@ -16,6 +17,18 @@ funDecToString ("" ⟨ x ⟩) = "function(" ++ varDecToString x ++ ")"
 funDecToString (f ⟨ x ⟩∈ T) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ "): " ++ typeToString T
 funDecToString (f ⟨ x ⟩) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ ")"
 
+binOpToString : BinaryOperator → String
+binOpToString + = "+"
+binOpToString - = "-"
+binOpToString * = "*"
+binOpToString / = "/"
+binOpToString < = "<"
+binOpToString > = ">"
+binOpToString ≡ = "=="
+binOpToString ≅ = "~="
+binOpToString ≤ = "<="
+binOpToString ≥ = ">="
+
 exprToString′ : ∀ {a} → String → Expr a → String
 statToString′ : ∀ {a} → String → Stat a → String
 blockToString′ : ∀ {a} → String → Block a → String
@@ -36,6 +49,10 @@ exprToString′ lb (block b is B end) =
   "(" ++ b ++ "()" ++ lb ++
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
   "end)()"
+exprToString′ lb (number x) = primShowFloat x
+exprToString′ lb (binexp x op y) = exprToString′ lb x ++ " " ++ binOpToString op ++ " " ++ exprToString′ lb y
+exprToString′ lb true = "true"
+exprToString′ lb false = "false"
 
 statToString′ lb (function F is B end) =
   "local " ++ funDecToString F ++ lb ++
diff --git a/prototyping/Luau/Type.agda b/prototyping/Luau/Type.agda
index 6e384c3b..af5f857c 100644
--- a/prototyping/Luau/Type.agda
+++ b/prototyping/Luau/Type.agda
@@ -7,6 +7,7 @@ data Type : Set where
   _⇒_ : Type → Type → Type
   none : Type
   any : Type
+  number : Type
   _∪_ : Type → Type → Type
   _∩_ : Type → Type → Type
 
@@ -15,6 +16,7 @@ src nil = none
 src (S ⇒ T) = S
 src none = none
 src any = any
+src number = none
 src (S ∪ T) = (src S) ∪ (src T)
 src (S ∩ T) = (src S) ∩ (src T)
 
@@ -23,6 +25,7 @@ tgt nil = none
 tgt (S ⇒ T) = T
 tgt none = none
 tgt any = any
+tgt number = none
 tgt (S ∪ T) = (tgt S) ∪ (tgt T)
 tgt (S ∩ T) = (tgt S) ∩ (tgt T)
 
@@ -40,4 +43,3 @@ normalizeOptional (S ∪ T) | S′         | nil        = optional S′
 normalizeOptional (S ∪ T) | nil        | T′         = optional T′
 normalizeOptional (S ∪ T) | S′         | T′         = S′ ∪ T′
 normalizeOptional T = T
-
diff --git a/prototyping/Luau/Type/FromJSON.agda b/prototyping/Luau/Type/FromJSON.agda
index 45bda5f3..49f74626 100644
--- a/prototyping/Luau/Type/FromJSON.agda
+++ b/prototyping/Luau/Type/FromJSON.agda
@@ -1,11 +1,11 @@
 module Luau.Type.FromJSON where
 
-open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any)
+open import Luau.Type using (Type; nil; _⇒_; _∪_; _∩_; any; number)
 
 open import Agda.Builtin.List using (List; _∷_; [])
+open import Agda.Builtin.Bool using (true; false)
 
 open import FFI.Data.Aeson using (Value; Array; Object; object; array; string; fromString; lookup)
-open import FFI.Data.Bool using (true; false)
 open import FFI.Data.Either using (Either; Left; Right)
 open import FFI.Data.Maybe using (Maybe; nothing; just)
 open import FFI.Data.String using (String; _++_)
@@ -41,6 +41,7 @@ typeFromJSON (object o) | just (string "AstTypeFunction") | nothing | nothing =
 typeFromJSON (object o) | just (string "AstTypeReference") with lookup name o
 typeFromJSON (object o) | just (string "AstTypeReference") | just (string "nil") = Right nil
 typeFromJSON (object o) | just (string "AstTypeReference") | just (string "any") = Right any
+typeFromJSON (object o) | just (string "AstTypeReference") | just (string "number") = Right number
 typeFromJSON (object o) | just (string "AstTypeReference") | _ = Left "Unknown referenced type"
 
 typeFromJSON (object o) | just (string "AstTypeUnion") with lookup types o
diff --git a/prototyping/Luau/Type/ToString.agda b/prototyping/Luau/Type/ToString.agda
index 698d6e8e..e7a7c1c0 100644
--- a/prototyping/Luau/Type/ToString.agda
+++ b/prototyping/Luau/Type/ToString.agda
@@ -1,7 +1,7 @@
 module Luau.Type.ToString where
 
 open import FFI.Data.String using (String; _++_)
-open import Luau.Type using (Type; nil; _⇒_; none; any; _∪_; _∩_; normalizeOptional)
+open import Luau.Type using (Type; nil; _⇒_; none; any; number; _∪_; _∩_; normalizeOptional)
 
 {-# TERMINATING #-}
 typeToString : Type → String
@@ -12,6 +12,7 @@ typeToString nil = "nil"
 typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T)
 typeToString none = "none"
 typeToString any = "any"
+typeToString number = "number"
 typeToString (S ∪ T) with normalizeOptional(S ∪ T)
 typeToString (S ∪ T) | ((S′ ⇒ T′) ∪ nil) = "(" ++ typeToString (S′ ⇒ T′) ++ ")?"
 typeToString (S ∪ T) | (S′ ∪ nil) = typeToString S′ ++ "?"
diff --git a/prototyping/Luau/Value.agda b/prototyping/Luau/Value.agda
index 4768f859..ed51abd7 100644
--- a/prototyping/Luau/Value.agda
+++ b/prototyping/Luau/Value.agda
@@ -1,15 +1,20 @@
 module Luau.Value where
 
+open import Agda.Builtin.Bool using (Bool; true; false)
+open import Agda.Builtin.Float using (Float)
 open import Luau.Addr using (Addr)
-open import Luau.Syntax using (Block; Expr; nil; addr)
+open import Luau.Syntax using (Block; Expr; nil; addr; number; true; false)
 open import Luau.Var using (Var)
 
 data Value : Set where
   nil : Value
   addr : Addr → Value
+  number : Float → Value
+  bool : Bool → Value
 
 val : ∀ {a} → Value → Expr a
 val nil = nil
 val (addr a) = addr a
-
-
+val (number x) = number x
+val (bool false) = false
+val (bool true) = true
diff --git a/prototyping/Luau/Value/ToString.agda b/prototyping/Luau/Value/ToString.agda
index 3cac3ee7..3421d4cd 100644
--- a/prototyping/Luau/Value/ToString.agda
+++ b/prototyping/Luau/Value/ToString.agda
@@ -1,10 +1,14 @@
 module Luau.Value.ToString where
 
 open import Agda.Builtin.String using (String)
-open import Luau.Value using (Value; nil; addr)
+open import Agda.Builtin.Float using (primShowFloat)
+open import Agda.Builtin.Bool using (true; false)
+open import Luau.Value using (Value; nil; addr; number; bool)
 open import Luau.Addr.ToString using (addrToString)
 
 valueToString : Value → String
 valueToString nil = "nil"
 valueToString (addr a) = addrToString a
- 
+valueToString (number x) = primShowFloat x
+valueToString (bool false) = "false"
+valueToString (bool true) = "true"
diff --git a/prototyping/PrettyPrinter.agda b/prototyping/PrettyPrinter.agda
index 4a6c7dd6..fdad32d6 100644
--- a/prototyping/PrettyPrinter.agda
+++ b/prototyping/PrettyPrinter.agda
@@ -30,4 +30,3 @@ runString txt | (Right value) = runJSON value
 
 main : IO ⊤
 main = getContents >>= runString
-
diff --git a/prototyping/Properties.agda b/prototyping/Properties.agda
index b08a3a81..1a6f92fa 100644
--- a/prototyping/Properties.agda
+++ b/prototyping/Properties.agda
@@ -1,5 +1,7 @@
 module Properties where
 
+import Properties.Contradiction
 import Properties.Dec
+import Properties.Equality
 import Properties.Step
 import Properties.Remember
diff --git a/prototyping/Properties/Contradiction.agda b/prototyping/Properties/Contradiction.agda
new file mode 100644
index 00000000..e9a92ad5
--- /dev/null
+++ b/prototyping/Properties/Contradiction.agda
@@ -0,0 +1,9 @@
+module Properties.Contradiction where
+
+data ⊥ : Set where
+
+¬ : Set → Set
+¬ A = A → ⊥
+
+CONTRADICTION : ∀ {A : Set} → ⊥ → A
+CONTRADICTION ()
diff --git a/prototyping/Properties/Equality.agda b/prototyping/Properties/Equality.agda
new file mode 100644
index 00000000..c027bee3
--- /dev/null
+++ b/prototyping/Properties/Equality.agda
@@ -0,0 +1,23 @@
+module Properties.Equality where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Properties.Contradiction using (¬)
+
+sym : ∀ {A : Set} {a b : A} → (a ≡ b) → (b ≡ a)
+sym refl = refl
+
+trans : ∀ {A : Set} {a b c : A} → (a ≡ b) → (b ≡ c) → (a ≡ c)
+trans refl refl = refl
+
+cong : ∀ {A B : Set} {a b : A} (f : A → B) → (a ≡ b) → (f a ≡ f b)
+cong f refl = refl
+
+subst₁ : ∀ {A : Set} {a b : A} (F : A → Set) → (a ≡ b) → (F a) → (F b)
+subst₁ F refl x = x
+
+subst₂ : ∀ {A B : Set} {a b : A} {c d : B} (F : A → B → Set) → (a ≡ b) → (c ≡ d) → (F a c) → (F b d)
+subst₂ F refl refl x = x
+
+_≢_ : ∀ {A : Set} → A → A → Set
+(a ≢ b) = ¬(a ≡ b)
+
diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda
index eeda4ef2..69dbac84 100644
--- a/prototyping/Properties/Step.agda
+++ b/prototyping/Properties/Step.agda
@@ -1,13 +1,16 @@
 module Properties.Step where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.Float using (primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv)
+open import Agda.Builtin.Bool using (true; false)
 open import FFI.Data.Maybe using (just; nothing)
 open import Luau.Heap using (Heap; _[_]; alloc; ok; function_is_end)
-open import Luau.Syntax using (Block; Expr; nil; var; addr; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg)
-open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app ; beta; function; block; return; done; local; subst)
-open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; UnboundVariable; SEGV; app; block; local; return)
+open import Luau.Syntax using (Block; Expr; nil; var; addr; true; false; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number; binexp; +; ≅)
+open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app₁ ; app₂ ; beta; function; block; return; done; local; subst; binOpNumbers; evalNumOp; binOp₁; binOp₂; evalEqOp; evalNeqOp; binOpEquality; binOpInequality)
+open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; TypeMismatch; UnboundVariable; SEGV; app₁; app₂; block; local; return; bin₁; bin₂)
+open import Luau.RuntimeType using (function; number)
 open import Luau.Substitution using (_[_/_]ᴮ)
-open import Luau.Value using (nil; addr; val)
+open import Luau.Value using (nil; addr; val; number; bool)
 open import Properties.Remember using (remember; _,_)
 
 data StepResultᴮ {a} (H : Heap a) (B : Block a) : Set
@@ -30,13 +33,21 @@ stepᴮ : ∀ {a} H B → StepResultᴮ {a} H B
 stepᴱ H nil = value nil refl
 stepᴱ H (var x) = error (UnboundVariable x)
 stepᴱ H (addr a) = value (addr a) refl
+stepᴱ H (number x) = value (number x) refl
+stepᴱ H (true) = value (bool true) refl
+stepᴱ H (false) = value (bool false) refl
 stepᴱ H (M $ N) with stepᴱ H M
-stepᴱ H (M $ N) | step H′ M′ D = step H′ (M′ $ N) (app D)
-stepᴱ H (nil $ N) | value nil refl = error NilIsNotAFunction
-stepᴱ H (addr a $ N) | value (addr a) refl with remember (H [ a ])
-stepᴱ H (addr a $ N) | value (addr a) refl | (nothing , p) = error (app (SEGV a p))
-stepᴱ H (addr a $ N) | value (addr a) refl | (just(function F is B end) , p) = step H (block fun F is (local arg F ← N) ∙ B end) (beta p)
-stepᴱ H (M $ N) | error E = error (app E)
+stepᴱ H (M $ N) | step H′ M′ D = step H′ (M′ $ N) (app₁ D)
+stepᴱ H (_ $ N) | value V refl with stepᴱ H N
+stepᴱ H (_ $ N) | value V refl | step H′ N′ s = step H′ (val V $ N′) (app₂ s)
+stepᴱ H (_ $ _) | value nil refl | value W refl = error (app₁ (TypeMismatch function nil λ()))
+stepᴱ H (_ $ _) | value (number n) refl | value W refl = error (app₁ (TypeMismatch function (number n) λ()))
+stepᴱ H (_ $ _) | value (bool x) refl | value W refl = error (app₁ (TypeMismatch function (bool x) λ()))
+stepᴱ H (_ $ _) | value (addr a) refl | value W refl with remember (H [ a ])
+stepᴱ H (_ $ _) | value (addr a) refl | value W refl  | (nothing , p) = error (app₁ (SEGV a p))
+stepᴱ H (_ $ _) | value (addr a) refl | value W refl  | (just(function F is B end) , p) = step H (block fun F is B [ W / name (arg F) ]ᴮ end) (beta p)
+stepᴱ H (M $ N) | value V p | error E = error (app₂ E)
+stepᴱ H (M $ N) | error E = error (app₁ E)
 stepᴱ H (block b is B end) with stepᴮ H B
 stepᴱ H (block b is B end) | step H′ B′ D = step H′ (block b is B′ end) (block D)
 stepᴱ H (block b is (return _ ∙ B′) end) | return V refl = step H (val V) return
@@ -44,6 +55,22 @@ stepᴱ H (block b is done end) | done refl = step H nil done
 stepᴱ H (block b is B end) | error E = error (block b E)
 stepᴱ H (function F is C end) with alloc H (function F is C end)
 stepᴱ H function F is C end | ok a H′ p = step H′ (addr a) (function p)
+stepᴱ H (binexp x op y) with stepᴱ H x
+stepᴱ H (binexp x op y) | value x′ refl with stepᴱ H y
+-- Have to use explicit form for ≡ here because it's a heavily overloaded symbol
+stepᴱ H (binexp x Luau.Syntax.≡ y) | value x′ refl | value y′ refl = step H (val (evalEqOp x′ y′)) binOpEquality
+stepᴱ H (binexp x ≅ y) | value x′ refl | value y′ refl = step H (val (evalNeqOp x′ y′)) binOpInequality
+stepᴱ H (binexp x op y) | value (number x′) refl | value (number y′) refl = step H (val (evalNumOp x′ op y′)) binOpNumbers
+stepᴱ H (binexp x op y) | value (number x′) refl | step H′ y′ s = step H′ (binexp (number x′) op y′) (binOp₂ s)
+stepᴱ H (binexp x op y) | value (number x′) refl | error E = error (bin₂ E)
+stepᴱ H (binexp x op y) | value nil refl | _ = error (bin₁ (TypeMismatch number nil λ()))
+stepᴱ H (binexp x op y) | _ | value nil refl = error (bin₂ (TypeMismatch number nil λ()))
+stepᴱ H (binexp x op y) | value (addr a) refl | _ = error (bin₁ (TypeMismatch number (addr a) λ()))
+stepᴱ H (binexp x op y) | _ | value (addr a) refl = error (bin₂ (TypeMismatch number (addr a) λ()))
+stepᴱ H (binexp x op y) | value (bool x′) refl | _ = error (bin₁ (TypeMismatch number (bool x′) λ()))
+stepᴱ H (binexp x op y) | _ | value (bool y′) refl = error (bin₂ (TypeMismatch number (bool y′) λ()))
+stepᴱ H (binexp x op y) | step H′ x′ s = step H′ (binexp x′ op y) (binOp₁ s)
+stepᴱ H (binexp x op y) | error E = error (bin₁ E)
 
 stepᴮ H (function F is C end ∙ B) with alloc H (function F is C end)
 stepᴮ H (function F is C end ∙ B) | ok a H′ p = step H′ (B [ addr a / fun F ]ᴮ) (function p)
diff --git a/prototyping/README.md b/prototyping/README.md
index f1761d1c..965c9c49 100644
--- a/prototyping/README.md
+++ b/prototyping/README.md
@@ -25,3 +25,21 @@ and run!
 ```
   luau-ast Examples/SmokeTest.lua | ./PrettyPrinter
 ```
+
+## Testing
+
+We have a series of snapshot tests in the `Tests/` directory. You interact with the tests using the `tests` Python script in the `prototyping` directory. To simply run the tests, run:
+
+```sh
+tests --luau-cli ../build/luau-ast --build
+```
+
+This will build the test targets and run them. Run `tests --help` for information about all the command-line options.
+
+### Adding a new test
+
+To add a new test, add it to `Tests/{SUITE_NAME}/{CASE_NAME}`. You'll need an `in.lua` file and an `out.txt` file. The `in.lua` file is the input Luau source code, while the `out.txt` file is the expected output after running `luau-ast in.lua | test_executable`.
+
+### Updating a test
+
+If you make a change to the prototype that results in an expected change in behavior, you might want to update the test cases automatically. To do this, run `tests` with the `--accept-new-output` (`-a` for short) flag. Rather than diffing the output, this will overwrite the `out.txt` files for each test case with the actual result. Commit the resulting changes with your PR.
diff --git a/prototyping/Tests/Interpreter/binary_equality_bools/in.lua b/prototyping/Tests/Interpreter/binary_equality_bools/in.lua
new file mode 100644
index 00000000..c9c72dc6
--- /dev/null
+++ b/prototyping/Tests/Interpreter/binary_equality_bools/in.lua
@@ -0,0 +1 @@
+return true == false
diff --git a/prototyping/Tests/Interpreter/binary_equality_bools/out.txt b/prototyping/Tests/Interpreter/binary_equality_bools/out.txt
new file mode 100644
index 00000000..c508d536
--- /dev/null
+++ b/prototyping/Tests/Interpreter/binary_equality_bools/out.txt
@@ -0,0 +1 @@
+false
diff --git a/prototyping/Tests/Interpreter/binary_equality_numbers/in.lua b/prototyping/Tests/Interpreter/binary_equality_numbers/in.lua
new file mode 100644
index 00000000..4efc68a7
--- /dev/null
+++ b/prototyping/Tests/Interpreter/binary_equality_numbers/in.lua
@@ -0,0 +1 @@
+return 1 == 1
diff --git a/prototyping/Tests/Interpreter/binary_equality_numbers/out.txt b/prototyping/Tests/Interpreter/binary_equality_numbers/out.txt
new file mode 100644
index 00000000..27ba77dd
--- /dev/null
+++ b/prototyping/Tests/Interpreter/binary_equality_numbers/out.txt
@@ -0,0 +1 @@
+true
diff --git a/prototyping/Tests/Interpreter/binary_exps/in.lua b/prototyping/Tests/Interpreter/binary_exps/in.lua
new file mode 100644
index 00000000..0750f9e6
--- /dev/null
+++ b/prototyping/Tests/Interpreter/binary_exps/in.lua
@@ -0,0 +1 @@
+return 1 + 2 - 2 * 2 / 2
diff --git a/prototyping/Tests/Interpreter/binary_exps/out.txt b/prototyping/Tests/Interpreter/binary_exps/out.txt
new file mode 100644
index 00000000..d3827e75
--- /dev/null
+++ b/prototyping/Tests/Interpreter/binary_exps/out.txt
@@ -0,0 +1 @@
+1.0
diff --git a/prototyping/Tests/Interpreter/return_nil/in.lua b/prototyping/Tests/Interpreter/return_nil/in.lua
new file mode 100644
index 00000000..4e6ce2db
--- /dev/null
+++ b/prototyping/Tests/Interpreter/return_nil/in.lua
@@ -0,0 +1,5 @@
+local function foo(x)
+	return nil
+end
+
+return foo(nil)
diff --git a/prototyping/Tests/Interpreter/return_nil/out.txt b/prototyping/Tests/Interpreter/return_nil/out.txt
new file mode 100644
index 00000000..607602cf
--- /dev/null
+++ b/prototyping/Tests/Interpreter/return_nil/out.txt
@@ -0,0 +1 @@
+nil
diff --git a/prototyping/Examples/SmokeTestOutput.lua b/prototyping/Tests/PrettyPrinter/smoke_test/in.lua
similarity index 69%
rename from prototyping/Examples/SmokeTestOutput.lua
rename to prototyping/Tests/PrettyPrinter/smoke_test/in.lua
index e663534a..d26e3a0d 100644
--- a/prototyping/Examples/SmokeTestOutput.lua
+++ b/prototyping/Tests/PrettyPrinter/smoke_test/in.lua
@@ -1,12 +1,12 @@
 local function id(x)
-  return x
+	return x
 end
 local function comp(f)
-  return function(g)
-    return function(x)
-      return f(g(x))
-    end
-  end
+	return function(g)
+		return function(x)
+			return f(g(x))
+		end
+	end
 end
 local id2 = comp(id)(id)
 local nil2 = id2(nil)
@@ -15,4 +15,5 @@ local b : nil = nil
 local c : (nil) -> nil = nil
 local d : (any & nil) = nil
 local e : any? = nil
+local f : number = 123
 return id2(nil2)
diff --git a/prototyping/Examples/SmokeTest.lua b/prototyping/Tests/PrettyPrinter/smoke_test/out.txt
similarity index 92%
rename from prototyping/Examples/SmokeTest.lua
rename to prototyping/Tests/PrettyPrinter/smoke_test/out.txt
index e663534a..34e0c4fe 100644
--- a/prototyping/Examples/SmokeTest.lua
+++ b/prototyping/Tests/PrettyPrinter/smoke_test/out.txt
@@ -15,4 +15,5 @@ local b : nil = nil
 local c : (nil) -> nil = nil
 local d : (any & nil) = nil
 local e : any? = nil
+local f : number = 123.0
 return id2(nil2)
diff --git a/prototyping/Utility/Bool.agda b/prototyping/Utility/Bool.agda
new file mode 100644
index 00000000..1afffb0d
--- /dev/null
+++ b/prototyping/Utility/Bool.agda
@@ -0,0 +1,16 @@
+module Utility.Bool where
+
+open import Agda.Builtin.Bool using (Bool; true; false)
+
+not : Bool → Bool
+not false = true
+not true = false
+
+_or_ : Bool → Bool → Bool
+true or _ = true
+_ or true = true
+_ or _ = false
+
+_and_ : Bool → Bool → Bool
+true and true = true
+_ and _ = false
diff --git a/prototyping/tests.py b/prototyping/tests.py
new file mode 100755
index 00000000..20070ae0
--- /dev/null
+++ b/prototyping/tests.py
@@ -0,0 +1,197 @@
+#!/usr/bin/python
+
+import argparse
+import difflib
+import enum
+import os
+import os.path
+import subprocess
+import sys
+
+SUITES = ["interpreter", "prettyprinter"]
+IN_FILE_NAME = "in.lua"
+OUT_FILE_NAME = "out.txt"
+SUITE_EXE_NAMES = {
+    "interpreter": "Interpreter",
+    "prettyprinter": "PrettyPrinter",
+}
+
+SUITE_ENTRY_POINTS = {
+    "interpreter": "Interpreter.agda",
+    "prettyprinter": "PrettyPrinter.agda",
+}
+
+SUITE_ROOTS = {
+    "interpreter": "Tests/Interpreter",
+    "prettyprinter": "Tests/PrettyPrinter",
+}
+
+class TestResultStatus(enum.Enum):
+    CLI_ERROR = 0
+    EXE_ERROR = 1
+    DIFF_ERROR = 2
+    SUCCESS = 3
+    WROTE_NEW = 4
+
+class DiffFailure:
+    def __init__(self, expected, actual):
+        self.expected = expected
+        self.actual = actual
+    
+    def diff_text(self):
+        diff_generator = difflib.context_diff(self.expected.splitlines(), self.actual.splitlines(), fromfile="expected", tofile="actual", n=3)
+        return "".join(diff_generator)
+    
+    def diff_html(self):
+        differ = difflib.HtmlDiff(tabsize=4)
+        return differ.make_file(self.expected.splitlines(), self.actual.splitlines(), fromdesc="Expected", todesc="Actual", context=True, numlines=5)
+
+class TestCaseResult:
+    def __init__(self, suite, case, status, details):
+        self.suite = suite
+        self.case = case
+        self.status = status
+        self.details = details
+    
+    def did_pass(self):
+        return self.status == TestResultStatus.SUCCESS or self.status == TestResultStatus.WROTE_NEW
+    
+    def to_string(self):
+        prefix = f"[{self.suite}/{self.case}]: "
+        if self.status == TestResultStatus.CLI_ERROR:
+            return f"{prefix}CLI ERROR: {self.details}"
+        elif self.status == TestResultStatus.EXE_ERROR:
+            return f"{prefix}EXE ERROR: {self.details}"
+        elif self.status == TestResultStatus.DIFF_ERROR:
+            text_diff = self.details.diff_text()
+            return f"{prefix}FAILED:\n{text_diff}"
+        elif self.status == TestResultStatus.SUCCESS:
+            return f"{prefix}SUCCEEDED"
+        elif self.status == TestResultStatus.WROTE_NEW:
+            return f"{prefix}WROTE NEW RESULT"
+    
+    def write_artifact(self, artifact_root):
+        if self.status != TestResultStatus.DIFF_ERROR:
+            return
+
+        filename = f"{self.suite}-{self.case}.out.html"
+        path = os.path.join(artifact_root, filename)
+        html = self.details.diff_html()
+        with open(path, "w") as file:
+            file.write(html)
+
+parser = argparse.ArgumentParser(description="Runs prototype test cases")
+parser.add_argument("--luau-cli", "-l", dest="cli_location", required=True, help="The location of luau-cli")
+parser.add_argument("--root", "-r", dest="prototype_root", required=False, default=os.getcwd(), help="The root of the prototype")
+parser.add_argument("--build", "-b", dest="build", action="store_true", default=True, help="Whether to automatically build required test binaries")
+parser.add_argument("--suite", "-s", dest="suites", action="append", default=[], choices=SUITES, help="Which test suites to run")
+parser.add_argument("--case", "-c", dest="cases", action="append", default=[], help="Which test cases to run")
+parser.add_argument("--accept-new-output", "-a", dest="snapshot", action="store_true", default=False, help="Whether to write the new output to files, instead of diffing against it")
+parser.add_argument("--write-diff-failures", dest="write_diffs", action="store_true", default=False, help="Whether to write test failure diffs to files")
+parser.add_argument("--diff-failure-location", dest="diff_location", default=None, help="Where to write diff failure files to")
+
+def build_suite(root, suite):
+    entry_point = SUITE_ENTRY_POINTS.get(suite)
+    if entry_point is None:
+        return (False, "Invalid suite")
+    
+    result = subprocess.run(["~/.cabal/bin/agda", "--compile", entry_point], shell=True, cwd=root, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+    if result.returncode == 0:
+        return (True, None)
+    else:
+        return (False, result.stdout)
+
+def run_test(in_path, out_path, cli_path, exe_path, snapshot):
+    cli_result = subprocess.run([cli_path, in_path], capture_output=True)
+    if cli_result.returncode != 0:
+        return (TestResultStatus.CLI_ERROR, f"CLI error: {cli_result.stderr}")
+    
+    exe_result = subprocess.run(exe_path, input=cli_result.stdout, capture_output=True)
+    if exe_result.returncode != 0:
+        return (TestResultStatus.EXE_ERROR, f"Executable error; stdout:{exe_result.stdout}\n\nstderr: {exe_result.stderr}")
+    actual_result = exe_result.stdout.decode("utf-8")
+
+    if snapshot:
+        with open(out_path, "w") as out_file:
+            out_file.write(actual_result)
+            return (TestResultStatus.WROTE_NEW, None)
+    else:
+        with open(out_path, "r") as out_file:
+            expected_result = out_file.read()
+
+            if expected_result != actual_result:
+                return (TestResultStatus.DIFF_ERROR, DiffFailure(expected_result, actual_result))
+    
+    return (TestResultStatus.SUCCESS, None)
+
+def should_run_case(case_name, filters):
+    if len(filters) == 0:
+        return True
+
+    return any([f in case_name for f in filters])
+
+def run_test_suite(args, suite, suite_root, suite_exe):
+    results = []
+
+    for entry in os.listdir(suite_root):
+        if not should_run_case(entry, args.cases):
+            continue
+
+        case_path = os.path.join(suite_root, entry)
+        if os.path.isdir(case_path):
+            in_path = os.path.join(case_path, IN_FILE_NAME)
+            out_path = os.path.join(case_path, OUT_FILE_NAME)
+
+            if not os.path.exists(in_path) or not os.path.exists(out_path):
+                continue
+            
+            status, details = run_test(in_path, out_path, args.cli_location, suite_exe, args.snapshot)
+            result = TestCaseResult(suite, entry, status, details)
+            results.append(result)
+
+    return results
+
+def main():
+    args = parser.parse_args()
+
+    suites = args.suites if len(args.suites) > 0 else SUITES
+    root = os.path.abspath(args.prototype_root)
+
+    if args.build:
+        for suite in suites:
+            success, reason = build_suite(root, suite)
+
+            if not success:
+                print(f"Error building executable for test suite {suite}:\n{reason}")
+                sys.exit(1)
+            else:
+                print(f"Built executable for test suite {suite} successfully.")
+    
+    failed = False
+    for suite in suites:
+        suite_root = os.path.join(root, SUITE_ROOTS.get(suite))
+        suite_exe = os.path.join(root, SUITE_EXE_NAMES.get(suite))
+        print(f"Running test suite {suite}...")
+        results = run_test_suite(args, suite, suite_root, suite_exe)
+
+        passed = 0
+        total = len(results)
+
+        for result in results:
+            if result.did_pass():
+                passed += 1
+            else:
+                failed = True
+
+        print(f"Suite {suite} [{passed} / {total} passed]:")
+        for result in results:
+            print(result.to_string())
+
+            if args.write_diffs:
+                result.write_artifact(args.diff_location)
+    
+    if failed:
+        sys.exit(1)
+
+if __name__ == "__main__":
+    main()
diff --git a/rfcs/STATUS.md b/rfcs/STATUS.md
index 9a45afe0..72db2003 100644
--- a/rfcs/STATUS.md
+++ b/rfcs/STATUS.md
@@ -23,12 +23,6 @@ This document tracks unimplemented RFCs.
 
 **Status**: Implemented but depends on new transaction log implementation that is not fully live yet.
 
-## Default type parameters
-
-[RFC: Default type alias type parameters](https://github.com/Roblox/luau/blob/master/rfcs/syntax-default-type-alias-type-parameters.md)
-
-**Status**: Implemented but not fully rolled out yet.
-
 ## Singleton types
 
 [RFC: Singleton types](https://github.com/Roblox/luau/blob/master/rfcs/syntax-singleton-types.md)
diff --git a/rfcs/syntax-default-type-alias-type-parameters.md b/rfcs/syntax-default-type-alias-type-parameters.md
index 15d23c81..443bbac3 100644
--- a/rfcs/syntax-default-type-alias-type-parameters.md
+++ b/rfcs/syntax-default-type-alias-type-parameters.md
@@ -1,5 +1,7 @@
 # Default type alias type parameters
 
+**Status**: Implemented
+
 ## Summary
 
 Introduce syntax to provide default type values inside the type alias type parameter list.
diff --git a/tests/Conformance.test.cpp b/tests/Conformance.test.cpp
index b09c1efb..23e90f4d 100644
--- a/tests/Conformance.test.cpp
+++ b/tests/Conformance.test.cpp
@@ -712,6 +712,47 @@ TEST_CASE("Reference")
     CHECK(dtorhits == 2);
 }
 
+TEST_CASE("ApiTables")
+{
+    StateRef globalState(luaL_newstate(), lua_close);
+    lua_State* L = globalState.get();
+
+    lua_newtable(L);
+    lua_pushnumber(L, 123.0);
+    lua_setfield(L, -2, "key");
+    lua_pushstring(L, "test");
+    lua_rawseti(L, -2, 5);
+
+    // lua_gettable
+    lua_pushstring(L, "key");
+    CHECK(lua_gettable(L, -2) == LUA_TNUMBER);
+    CHECK(lua_tonumber(L, -1) == 123.0);
+    lua_pop(L, 1);
+
+    // lua_getfield
+    CHECK(lua_getfield(L, -1, "key") == LUA_TNUMBER);
+    CHECK(lua_tonumber(L, -1) == 123.0);
+    lua_pop(L, 1);
+
+    // lua_rawgetfield
+    CHECK(lua_rawgetfield(L, -1, "key") == LUA_TNUMBER);
+    CHECK(lua_tonumber(L, -1) == 123.0);
+    lua_pop(L, 1);
+
+    // lua_rawget
+    lua_pushstring(L, "key");
+    CHECK(lua_rawget(L, -2) == LUA_TNUMBER);
+    CHECK(lua_tonumber(L, -1) == 123.0);
+    lua_pop(L, 1);
+
+    // lua_rawgeti
+    CHECK(lua_rawgeti(L, -1, 5) == LUA_TSTRING);
+    CHECK(strcmp(lua_tostring(L, -1), "test") == 0);
+    lua_pop(L, 1);
+
+    lua_pop(L, 1);
+}
+
 TEST_CASE("ApiFunctionCalls")
 {
     StateRef globalState = runConformance("apicalls.lua");