diff --git a/primer/src/Primer/Eval/NormalOrder.hs b/primer/src/Primer/Eval/NormalOrder.hs
index 73508b5c0..f2ab98b11 100644
--- a/primer/src/Primer/Eval/NormalOrder.hs
+++ b/primer/src/Primer/Eval/NormalOrder.hs
@@ -45,6 +45,8 @@ import Primer.Core (
     App,
     Case,
     Hole,
+    LAM,
+    Lam,
     Let,
     LetType,
     Letrec
@@ -139,6 +141,7 @@ viewLet dez@(_, ez) = case (target ez, exprChildren' dez) of
 
 data NormalOrderOptions -- TODO/REVIEW: this is a bit of a misnomer, as it affects `Eval.redexes`, which is only used for single-step. NB: even if we set StopAtBinders, we can still call `Eval.step` with the id of a redex under a binder and it will reduce, even though `redexes` will not report that id
   = UnderBinders
+  | StopAtBinders
   deriving stock (Eq, Show, Read, Generic)
   deriving (FromJSON, ToJSON) via PrimerJSON NormalOrderOptions
 
@@ -330,9 +333,21 @@ exprChildren' (d, ez) =
     addBinds ez bs
     pure (d', c)
 
+-- Extract the children of the current focus, except those under an "unknown" binder,
+-- i.e. we extract the body of a let but not the body of a lambda, or the RHS of case branches.
+-- This is used to restrict our evaluation to "closed evaluation".
+-- NB: for consistency we skip all case branches, not just those that bind a variable.
+exprChildrenClosed :: (Dir, ExprZ) -> [Accum Cxt (Dir, ExprZ)]
+exprChildrenClosed (d, ez) = case target ez of
+  Lam{} -> []
+  LAM{} -> []
+  Case{} -> take 1 $ exprChildren' (d, ez) -- just the scrutinee
+  _ -> exprChildren' (d, ez)
+
 exprChildren :: NormalOrderOptions -> (Dir, ExprZ) -> [Accum Cxt (Dir, ExprZ)]
 exprChildren = \case
   UnderBinders -> exprChildren'
+  StopAtBinders -> exprChildrenClosed
 
 typeChildren :: TypeZ -> [Accum Cxt TypeZ]
 typeChildren tz =
diff --git a/primer/test/Tests/Eval.hs b/primer/test/Tests/Eval.hs
index a80b3b782..19cb5916e 100644
--- a/primer/test/Tests/Eval.hs
+++ b/primer/test/Tests/Eval.hs
@@ -58,7 +58,7 @@ import Primer.Eval (
   GlobalVarInlineDetail (..),
   LetRemovalDetail (..),
   LocalVarInlineDetail (..),
-  NormalOrderOptions (UnderBinders),
+  NormalOrderOptions (StopAtBinders, UnderBinders),
   findNodeByID,
   getNonCapturedLocal,
   redexes,
@@ -1430,7 +1430,7 @@ tasty_type_preservation =
             let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules
             tds <- asks typeDefs
             (dir, t, ty) <- genDirTm
-            closed <- forAllT $ Gen.element [UnderBinders]
+            closed <- forAllT $ Gen.element [UnderBinders, StopAtBinders]
             rs <- failWhenSevereLogs $ redexes @EvalLog closed tds globs dir t
             when (null rs) discard
             r <- forAllT $ Gen.element rs
@@ -1459,7 +1459,7 @@ tasty_redex_independent =
             (dir, t, _) <- genDirTm
             annotateShow dir
             annotateShow t
-            closed <- forAllT $ Gen.element [UnderBinders]
+            closed <- forAllT $ Gen.element [UnderBinders, StopAtBinders]
             rs <- failWhenSevereLogs $ redexes @EvalLog closed tds globs dir t
             when (length rs <= 1) discard
             i <- forAllT $ Gen.element rs
diff --git a/primer/test/Tests/Eval/Utils.hs b/primer/test/Tests/Eval/Utils.hs
index 9764346f7..2418c77cf 100644
--- a/primer/test/Tests/Eval/Utils.hs
+++ b/primer/test/Tests/Eval/Utils.hs
@@ -4,6 +4,7 @@ module Tests.Eval.Utils (
   genDirTm,
   testModules,
   hasTypeLets,
+  hasHoles,
 ) where
 
 import Foreword
@@ -15,12 +16,12 @@ import Hedgehog (PropertyT)
 import Hedgehog.Gen qualified as Gen
 import Primer.Core (
   Expr,
-  Expr' (LetType),
+  Expr' (EmptyHole, Hole, LetType),
   ID,
   Kind (KType),
   ModuleName (ModuleName),
   Type,
-  Type' (TLet),
+  Type' (TEmptyHole, THole, TLet),
  )
 import Primer.Core.DSL (create', lam, lvar, tcon, tfun)
 import Primer.Core.Utils (forgetMetadata, forgetTypeMetadata, generateIDs)
@@ -98,3 +99,12 @@ hasTypeLets e =
   not $
     null [() | LetType{} <- universe e]
       && null [() | TLet{} <- universeBi @_ @Type e]
+
+-- | Does this expression have any holes?
+hasHoles :: Expr -> Bool
+hasHoles e =
+  not $
+    null [() | Hole{} <- universe e]
+      && null [() | EmptyHole{} <- universe e]
+      && null [() | THole{} <- universeBi @_ @Type e]
+      && null [() | TEmptyHole{} <- universeBi @_ @Type e]
diff --git a/primer/test/Tests/EvalFull.hs b/primer/test/Tests/EvalFull.hs
index 11e958dfd..462642d7e 100644
--- a/primer/test/Tests/EvalFull.hs
+++ b/primer/test/Tests/EvalFull.hs
@@ -22,6 +22,7 @@ import Primer.App (
  )
 import Primer.Builtins (
   boolDef,
+  cCons,
   cFalse,
   cJust,
   cMakePair,
@@ -41,16 +42,17 @@ import Primer.Core.DSL
 import Primer.Core.Utils (
   exprIDs,
   forgetMetadata,
+  generateIDs,
  )
 import Primer.Def (DefMap)
-import Primer.Eval (NormalOrderOptions (UnderBinders))
+import Primer.Eval (NormalOrderOptions (StopAtBinders, UnderBinders))
 import Primer.EvalFull
 import Primer.Examples qualified as Examples (
   even,
   map',
   odd,
  )
-import Primer.Gen.Core.Typed (WT, forAllT, isolateWT, propertyWT)
+import Primer.Gen.Core.Typed (WT, forAllT, genChk, isolateWT, propertyWT)
 import Primer.Log (runPureLogT)
 import Primer.Module (
   Module (Module, moduleDefs, moduleName, moduleTypes),
@@ -119,7 +121,7 @@ import Tasty (
  )
 import Test.Tasty.HUnit (Assertion, assertBool, assertFailure, (@?=))
 import Tests.Action.Prog (readerToState)
-import Tests.Eval.Utils (genDirTm, hasTypeLets, testModules, (~=))
+import Tests.Eval.Utils (genDirTm, hasHoles, hasTypeLets, testModules, (~=))
 import Tests.Gen.Core.Typed (checkTest)
 import Tests.Typecheck (runTypecheckTestM, runTypecheckTestMWithPrims)
 
@@ -427,6 +429,110 @@ unit_tlet_self_capture = do
         r <~==> expect
    in mapM_ test (zip [0 ..] expected)
 
+-- When doing closed eval (i.e. don't go under binders), we still need to do
+-- substitution under binders, else @let@s can block redexes.
+unit_closed_let_beta :: Assertion
+unit_closed_let_beta =
+  let ((expr, expected), maxID) = create $ do
+        e0 <- let_ "x" (con0 cFalse `ann` tcon tBool) (lam "y" (con cCons [lvar "x", lvar "y"]) `ann` (tcon tBool `tfun` (tcon tList `tapp` tcon tBool))) `app` con0 cTrue
+        e1 <- let_ "x" (con0 cFalse `ann` tcon tBool) (lam "y" (con cCons [con0 cFalse `ann` tcon tBool, lvar "y"]) `ann` (tcon tBool `tfun` (tcon tList `tapp` tcon tBool))) `app` con0 cTrue
+        e2 <- (lam "y" (con cCons [con0 cFalse `ann` tcon tBool, lvar "y"]) `ann` (tcon tBool `tfun` (tcon tList `tapp` tcon tBool))) `app` con0 cTrue
+        e3 <- let_ "y" (con0 cTrue `ann` tcon tBool) (con cCons [con0 cFalse `ann` tcon tBool, lvar "y"]) `ann` (tcon tList `tapp` tcon tBool)
+        e4 <- let_ "y" (con0 cTrue `ann` tcon tBool) (con cCons [con0 cFalse `ann` tcon tBool, con0 cTrue `ann` tcon tBool]) `ann` (tcon tList `tapp` tcon tBool)
+        e5 <- con cCons [con0 cFalse `ann` tcon tBool, con0 cTrue `ann` tcon tBool] `ann` (tcon tList `tapp` tcon tBool)
+        e6 <- con cCons [con0 cFalse, con0 cTrue `ann` tcon tBool] `ann` (tcon tList `tapp` tcon tBool)
+        e7 <- con cCons [con0 cFalse, con0 cTrue] `ann` (tcon tList `tapp` tcon tBool)
+        pure (e0, map (Left . TimedOut) [e0, e1, e2, e3, e4, e5, e6, e7] ++ [Right e7])
+      test (n, expect) = do
+        r <- evalFullTestClosed maxID mempty mempty n Syn expr
+        r <~==> expect
+   in mapM_ test (zip [0 ..] expected)
+
+-- One reason for not evaluating under binders is to avoid a size blowup when
+-- evaluating a recursive definition. For example, the unsaturated
+-- `map @Bool @Bool not` would keep unrolling the recursive mentions of `map`.
+-- (If it were applied to a concrete list, the beta redexes would be reduced instead.)
+-- Since top-level definitions and recursive lets are essentially the same, and
+-- we do substitution of @let@s under binders, one may worry that we have the same
+-- issue with @letrec@. This test shows that we do not.
+unit_closed_letrec_binder :: Assertion
+unit_closed_letrec_binder =
+  let ((expr, expected), maxID) = create $ do
+        e0 <- letrec "x" (list_ [lvar "x", lvar "x"]) (tcon tBool) $ lam "y" $ lvar "x"
+        e1 <-
+          letrec "x" (list_ [lvar "x", lvar "x"]) (tcon tBool) $
+            lam "y" $
+              letrec "x" (list_ [lvar "x", lvar "x"]) (tcon tBool) $
+                list_ [lvar "x", lvar "x"] `ann` tcon tBool
+        e2 <- lam "y" $ letrec "x" (list_ [lvar "x", lvar "x"]) (tcon tBool) $ list_ [lvar "x", lvar "x"] `ann` tcon tBool
+        pure (e0, map (Left . TimedOut) [e0, e1, e2] ++ [Right e2])
+      test (n, expect) = do
+        r <- evalFullTestClosed maxID mempty mempty n Syn expr
+        r <~==> expect
+   in mapM_ test (zip [0 ..] expected)
+
+-- closed eval stops at binders
+unit_closed_binders :: Assertion
+unit_closed_binders = do
+  let isNormalIffClosed e = do
+        let (e', i) = create e
+        evalFullTestClosed i mempty mempty 1 Syn e' >>= \case
+          Left (TimedOut _) -> assertFailure $ "not normal form, for closed eval: " <> show e'
+          Right _ -> pure ()
+        evalFullTest i mempty mempty 1 Syn e' >>= \case
+          Left (TimedOut _) -> pure ()
+          Right _ -> assertFailure $ "unexpectedly a normal form, for open eval: " <> show e'
+      r = let_ "x" emptyHole $ lvar "x"
+  isNormalIffClosed $ lam "x" r
+  isNormalIffClosed $ lAM "a" r
+  isNormalIffClosed $ case_ emptyHole [branch cTrue [("x", Nothing)] r]
+  -- For consistency, we also do not reduce inside case branches even if they do not bind
+  isNormalIffClosed $ case_ emptyHole [branch cTrue [] r]
+
+-- closed eval still substitutes under binders
+-- (otherwise we might not be able to elide a let which blocks a redex -- see
+-- unit_closed_let_beta)
+unit_closed_subst :: Assertion
+unit_closed_subst = do
+  let isReducible e = do
+        let (e', i) = create e
+        evalFullTestClosed i mempty mempty 1 Syn e' >>= \case
+          Left (TimedOut _) -> pure ()
+          Right _ -> assertFailure $ "unexpectedly a normal form: " <> show e'
+      l = let_ "x" emptyHole
+      v = lvar "x"
+  isReducible $ l $ lam "y" v
+  isReducible $ l $ lAM "a" v
+  isReducible $ l $ case_ emptyHole [branch cTrue [("x", Nothing)] v]
+  isReducible $ l $ case_ emptyHole [branch cTrue [] v]
+
+-- For (closed, hole free) terms of base types, open and closed evaluation
+-- agree.  We require hole-free-ness, as holes create stuck terms similar to
+-- free variables. Note that we get the same reduction sequence, not only that
+-- they reduce to the same value.
+tasty_open_closed_agree_base_types :: Property
+tasty_open_closed_agree_base_types = withDiscards 1000 $
+  propertyWT testModules $ do
+    ty <- forAllT $ Gen.element [tBool, tNat, tInt]
+    tm' <- forAllT $ genChk $ TCon () ty
+    tm <- generateIDs tm'
+    when (hasHoles tm) discard
+    tds <- asks typeDefs
+    let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules
+    let reductionSequence closed expr n =
+          (expr :)
+            <$> if n <= (0 :: Integer)
+              then pure []
+              else
+                evalFull @EvalLog closed tds globs 1 Chk expr >>= \case
+                  Left (TimedOut expr') -> reductionSequence closed expr' (n - 1)
+                  Right _ -> pure []
+    (openSeq, openLogs) <- lift $ isolateWT $ runPureLogT $ reductionSequence UnderBinders tm 100
+    testNoSevereLogs openLogs
+    (closedSeq, closedLogs) <- lift $ isolateWT $ runPureLogT $ reductionSequence StopAtBinders tm 100
+    testNoSevereLogs closedLogs
+    openSeq === closedSeq
+
 -- TODO: examples with holes
 
 -- TODO: most of these property tests could benefit from generating an
@@ -447,7 +553,7 @@ resumeTest mods dir t = do
   let globs = foldMap' moduleDefsQualified mods
   tds <- asks typeDefs
   n <- forAllT $ Gen.integral $ Range.linear 2 1000 -- Arbitrary limit here
-  closed <- forAllT $ Gen.element [UnderBinders]
+  closed <- forAllT $ Gen.element [UnderBinders, StopAtBinders]
   -- NB: We need to run this first reduction in an isolated context
   -- as we need to avoid it changing the fresh-name-generator state
   -- for the next run (sMid and sTotal). This is because reduction may need
@@ -822,7 +928,7 @@ tasty_type_preservation = withTests 1000 $
                 s' <- checkTest ty s
                 forgetMetadata s === forgetMetadata s' -- check no smart holes happened
       maxSteps <- forAllT $ Gen.integral $ Range.linear 1 1000 -- Arbitrary limit here
-      closed <- forAllT $ Gen.element [UnderBinders]
+      closed <- forAllT $ Gen.element [UnderBinders, StopAtBinders]
       (steps, s) <- failWhenSevereLogs $ evalFullStepCount @EvalLog closed tds globs maxSteps dir t
       annotateShow steps
       annotateShow s
@@ -1340,7 +1446,7 @@ tasty_unique_ids = withTests 1000 $
       let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules
       tds <- asks typeDefs
       (dir, t1, _) <- genDirTm
-      closed <- forAllT $ Gen.element [UnderBinders]
+      closed <- forAllT $ Gen.element [UnderBinders, StopAtBinders]
       let go n t
             | n == (0 :: Int) = pure ()
             | otherwise = do
@@ -1418,6 +1524,13 @@ evalFullTest id_ tydefs globals n d e = do
   distinctIDs r
   pure r
 
+evalFullTestClosed :: ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> IO (Either EvalFullError Expr)
+evalFullTestClosed id_ tydefs globals n d e = do
+  let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog StopAtBinders tydefs globals n d e
+  assertNoSevereLogs logs
+  distinctIDs r
+  pure r
+
 evalFullTasty :: MonadTest m => ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> m (Either EvalFullError Expr)
 evalFullTasty id_ tydefs globals n d e = do
   let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog UnderBinders tydefs globals n d e