diff --git a/src/Init/Data/Char/Basic.lean b/src/Init/Data/Char/Basic.lean
index c08b18437b..86ee470c41 100644
--- a/src/Init/Data/Char/Basic.lean
+++ b/src/Init/Data/Char/Basic.lean
@@ -5,6 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.UInt
+
 @[inline, reducible] def isValidChar (n : UInt32) : Prop :=
 n < 0xd800 ∨ (0xdfff < n ∧ n < 0x110000)
 
@@ -19,14 +20,10 @@ instance : HasSizeof Char :=
 namespace Char
 def utf8Size (c : Char) : UInt32 :=
 let v := c.val;
-     if UInt32.land v 0x80 = 0    then 1
-else if UInt32.land v 0xE0 = 0xC0 then 2
-else if UInt32.land v 0xF0 = 0xE0 then 3
-else if UInt32.land v 0xF8 = 0xF0 then 4
-else if UInt32.land v 0xFC = 0xF8 then 5
-else if UInt32.land v 0xFE = 0xFC then 6
-else if v = 0xFF                  then 1
-else 0
+if v < 0x7F then 1
+else if v < 0x7FF then 2
+else if v < 0xFFFF then 3
+else 4
 
 protected def Less (a b : Char) : Prop := a.val < b.val
 protected def LessEq (a b : Char) : Prop := a.val ≤ b.val
diff --git a/src/Init/Data/UInt.lean b/src/Init/Data/UInt.lean
index ebca55d798..c2c3ef5e37 100644
--- a/src/Init/Data/UInt.lean
+++ b/src/Init/Data/UInt.lean
@@ -186,6 +186,11 @@ def UInt32.decLe (a b : UInt32) : Decidable (a ≤ b) :=
 UInt32.casesOn a $ fun n => UInt32.casesOn b $ fun m =>
   inferInstanceAs (Decidable (n <= m))
 
+@[extern c inline "#1 << #2"]
+constant UInt32.shiftLeft (a b : UInt32) : UInt32 := (arbitrary Nat).toUInt32
+@[extern c inline "#1 >> #2"]
+constant UInt32.shiftRight (a b : UInt32) : UInt32 := (arbitrary Nat).toUInt32
+
 instance : DecidableEq UInt32 := UInt32.decEq
 instance UInt32.hasDecidableLt (a b : UInt32) : Decidable (a < b) := UInt32.decLt a b
 instance UInt32.hasDecidableLe (a b : UInt32) : Decidable (a ≤ b) := UInt32.decLe a b
diff --git a/src/Init/Lean/Data/Options.lean b/src/Init/Lean/Data/Options.lean
index 679cbe41e2..4d4ef976d7 100644
--- a/src/Init/Lean/Data/Options.lean
+++ b/src/Init/Lean/Data/Options.lean
@@ -64,7 +64,7 @@ pure decl.descr
 
 def setOptionFromString (opts : Options) (entry : String) : IO Options := do
 let ps := (entry.splitOn "=").map String.trim;
-[key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form '<key> = <value>'";
+[key, val] ← pure ps | throw $ IO.userError "invalid configuration option entry, it must be of the form '<key> = <value>'";
 defValue ← getOptionDefaulValue key.toName;
 match defValue with
 | DataValue.ofString v => pure $ opts.setString key val
diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index 254cbd1950..fa282e56d0 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/src/Init/Lean/Elab/Command.lean
@@ -168,7 +168,7 @@ registerBuiltinAttribute {
    unless persistent $ throw (IO.userError ("invalid attribute 'builtinCommandElab', must be persistent"));
    kind ← IO.ofExcept $ syntaxNodeKindOfAttrParam env `Lean.Parser.Command arg;
    match env.find? declName with
-   | none  => throw "unknown declaration"
+   | none  => throw $ IO.userError "unknown declaration"
    | some decl =>
      match decl.type with
      | Expr.const `Lean.Elab.Command.CommandElab _ _ => declareBuiltinCommandElab env kind declName
diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 0440377647..524f297131 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -203,7 +203,7 @@ registerBuiltinAttribute {
    unless persistent $ throw (IO.userError ("invalid attribute 'builtinTermElab', must be persistent"));
    kind ← IO.ofExcept $ syntaxNodeKindOfAttrParam env `Lean.Parser.Term arg;
    match env.find? declName with
-   | none  => throw "unknown declaration"
+   | none  => throw $ IO.userError "unknown declaration"
    | some decl =>
      match decl.type with
      | Expr.const `Lean.Elab.Term.TermElab _ _ => declareBuiltinTermElab env kind declName
diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index 3cf208274a..4fa4fc26bd 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -1639,7 +1639,7 @@ private def BuiltinParserAttribute.add (attrName : Name) (catName : Name)
 when args.hasArgs $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', unexpected argument"));
 unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', must be persistent"));
 match env.find? declName with
-| none  => throw "unknown declaration"
+| none  => throw $ IO.userError "unknown declaration"
 | some decl =>
   match decl.type with
  | Expr.const `Lean.Parser.TrailingParser _ _ =>
diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 60c4a9485a..716250ffe9 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -6,6 +6,8 @@ Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich
 prelude
 import Init.Control.EState
 import Init.Data.String.Basic
+import Init.Data.ByteArray
+import Init.System.IOError
 import Init.System.FilePath
 
 /-- Like https://hackage.haskell.org/package/ghc-Prim-0.5.2.0/docs/GHC-Prim.html#t:RealWorld.
@@ -37,22 +39,6 @@ instance (α ε : Type) : HasOrelse (EIO ε α) := ⟨MonadExcept.orelse⟩
 instance {ε : Type} {α : Type} [Inhabited ε] : Inhabited (EIO ε α) :=
 inferInstanceAs (Inhabited (EStateM ε IO.RealWorld α))
 
-/-
-In the future, we may want to give more concrete data
-like in https://doc.rust-lang.org/std/IO/enum.ErrorKind.html
--/
-def IO.Error := String
-
-instance : HasToString IO.Error := inferInstanceAs (HasToString String)
-instance : Inhabited IO.Error := inferInstanceAs (Inhabited String)
-
-def IO.userError (s : String) : IO.Error :=
-s
-
-@[export lean_io_error_to_string]
-def IO.Error.toString : IO.Error → String :=
-id
-
 abbrev IO : Type → Type := EIO IO.Error
 
 section
@@ -96,18 +82,29 @@ pure (fn ())
 inductive FS.Mode
 | read | write | readWrite | append
 
-constant FS.handle : Type := Unit
+constant FS.Handle : Type := Unit
 
 namespace Prim
 open FS
 
 @[specialize] partial def iterate {α β : Type} : α → (α → IO (Sum α β)) → IO β
-| a, f =>
-  do v ← f a;
+| a, f => do
+  v ← f a;
   match v with
   | Sum.inl a => iterate a f
   | Sum.inr b => pure b
 
+-- @[export lean_fopen_flags]
+def fopenFlags (m : FS.Mode) (b : Bool) : String :=
+let mode :=
+  match m with
+  | FS.Mode.read      => "r"
+  | FS.Mode.write     => "w"
+  | FS.Mode.readWrite => "r+"
+  | FS.Mode.append    => "a" ;
+let bin := if b then "b" else "t";
+mode ++ bin
+
 @[extern "lean_io_prim_put_str"]
 constant putStr (s: @& String) : IO Unit := arbitrary _
 @[extern "lean_io_prim_read_text_file"]
@@ -115,18 +112,26 @@ constant readTextFile (s : @& String) : IO String := arbitrary _
 @[extern "lean_io_prim_get_line"]
 constant getLine : IO String := arbitrary _
 @[extern "lean_io_prim_handle_mk"]
-constant handle.mk (s : @& String) (m : Mode) (bin : Bool := false) : IO handle := arbitrary _
+constant Handle.mk (s : @& String) (mode : @& String) : IO Handle := arbitrary _
 @[extern "lean_io_prim_handle_is_eof"]
-constant handle.isEof (h : @& handle) : IO Bool := arbitrary _
+constant Handle.isEof (h : @& Handle) : IO Bool := arbitrary _
 @[extern "lean_io_prim_handle_flush"]
-constant handle.flush (h : @& handle) : IO Unit := arbitrary _
-@[extern "lean_io_prim_handle_close"]
-constant handle.close (h : @& handle) : IO Unit := arbitrary _
+constant Handle.flush (h : @& Handle) : IO Unit := arbitrary _
 -- TODO: replace `String` with byte buffer
--- constant handle.read : handle → Nat → EIO String
--- constant handle.write : handle → String → EIO Unit
+@[extern "lean_io_prim_handle_read"]
+constant Handle.read  (h : @& Handle) (bytes : USize) : IO ByteArray := arbitrary _
+@[extern "lean_io_prim_handle_write"]
+constant Handle.write (h : @& Handle) (buffer : @& ByteArray) : IO Unit := arbitrary _
+
+@[extern "lean_io_prim_handle_read_byte"]
+constant Handle.getByte  (h : @& Handle) : IO UInt8 := arbitrary _
+@[extern "lean_io_prim_handle_write_byte"]
+constant Handle.putByte (h : @& Handle) (c : UInt8) : IO Unit := arbitrary _
+
 @[extern "lean_io_prim_handle_get_line"]
-constant handle.getLine (h : @& handle) : IO String := arbitrary _
+constant Handle.getLine (h : @& Handle) : IO String := arbitrary _
+@[extern "lean_io_prim_handle_put_str"]
+constant Handle.putStr (h : @& Handle) (s : @& String) : IO Unit := arbitrary _
 
 @[extern "lean_io_getenv"]
 constant getEnv (var : @& String) : IO (Option String) := arbitrary _
@@ -167,31 +172,33 @@ end
 namespace FS
 variables {m : Type → Type} [Monad m] [MonadIO m]
 
-def handle.mk (s : String) (Mode : Mode) (bin : Bool := false) : m handle := Prim.liftIO (Prim.handle.mk s Mode bin)
-def handle.isEof : handle → m Bool := Prim.liftIO ∘ Prim.handle.isEof
-def handle.flush : handle → m Unit := Prim.liftIO ∘ Prim.handle.flush
-def handle.close : handle → m Unit := Prim.liftIO ∘ Prim.handle.flush
--- def handle.read (h : handle) (bytes : Nat) : m String := Prim.liftEIO (Prim.handle.read h bytes)
--- def handle.write (h : handle) (s : String) : m Unit := Prim.liftEIO (Prim.handle.write h s)
-def handle.getLine : handle → m String := Prim.liftIO ∘ Prim.handle.getLine
+def Handle.mk (s : String) (Mode : Mode) (bin : Bool := false) : m Handle :=
+Prim.liftIO (Prim.Handle.mk s (Prim.fopenFlags Mode bin))
 
-/-
-def getChar (h : handle) : m Char := do
-b ← h.read 1,
-if b.isEmpty then fail "getChar failed"
-else pure b.mkIterator.curr
+@[inline]
+def withFile {α} (fn : String) (m : Mode) (f : Handle → IO α) : IO α :=
+Handle.mk fn m >>= f
+
+/-- returns whether the end of the file has been reached while reading a file.
+`h.isEof` returns true /after/ the first attempt at reading past the end of `h`.
+Once `h.isEof` is true, the reading `h` raises `IO.Error.eof`.
 -/
+def Handle.isEof : Handle → m Bool := Prim.liftIO ∘ Prim.Handle.isEof
+def Handle.flush : Handle → m Unit := Prim.liftIO ∘ Prim.Handle.flush
+def Handle.read (h : Handle) (bytes : Nat) : m ByteArray := Prim.liftIO (Prim.Handle.read h (USize.ofNat bytes))
+def Handle.write (h : Handle) (s : ByteArray) : m Unit := Prim.liftIO (Prim.Handle.write h s)
+def Handle.getByte (h : Handle) : m UInt8 := Prim.liftIO (Prim.Handle.getByte h)
+def Handle.putByte (h : Handle) (b : UInt8) : m Unit := Prim.liftIO (Prim.Handle.putByte h b)
 
--- def handle.putChar (h : handle) (c : Char) : m Unit :=
--- h.write (toString c)
+def Handle.getLine : Handle → m String := Prim.liftIO ∘ Prim.Handle.getLine
 
--- def handle.putStr (h : handle) (s : String) : m Unit :=
--- h.write s
+def Handle.putStr (h : Handle) (s : String) : m Unit :=
+Prim.liftIO $ Prim.Handle.putStr h s
 
--- def handle.putStrLn (h : handle) (s : String) : m Unit :=
--- h.putStr s *> h.putStr "\n"
+def Handle.putStrLn (h : Handle) (s : String) : m Unit :=
+h.putStr s *> h.putStr "\n"
 
-def handle.readToEnd (h : handle) : m String :=
+def Handle.readToEnd (h : Handle) : m String :=
 Prim.liftIO $ Prim.iterate "" $ fun r => do
   done ← h.isEof;
   if done
@@ -202,29 +209,28 @@ Prim.liftIO $ Prim.iterate "" $ fun r => do
     pure $ Sum.inl (r ++ c) -- continue
 
 def readFile (fname : String) (bin := false) : m String := do
-h ← handle.mk fname Mode.read bin;
+h ← Handle.mk fname Mode.read bin;
 r ← h.readToEnd;
-h.close;
 pure r
 
 end FS
 
--- constant stdin : IO FS.handle
--- constant stderr : IO FS.handle
--- constant stdout : IO FS.handle
+-- constant stdin : IO FS.Handle
+-- constant stderr : IO FS.Handle
+-- constant stdout : IO FS.Handle
 
 /-
 namespace Proc
 def child : Type :=
 MonadIOProcess.child ioCore
 
-def child.stdin : child → handle :=
+def child.stdin : child → Handle :=
 MonadIOProcess.stdin
 
-def child.stdout : child → handle :=
+def child.stdout : child → Handle :=
 MonadIOProcess.stdout
 
-def child.stderr : child → handle :=
+def child.stderr : child → Handle :=
 MonadIOProcess.stderr
 
 def spawn (p : IO.process.spawnArgs) : IO child :=
@@ -236,6 +242,34 @@ MonadIOProcess.wait c
 end Proc
 -/
 
+structure AccessRight :=
+(read write execution : Bool := false)
+
+def AccessRight.flags (acc : AccessRight) : UInt32 :=
+let r : UInt32 := if acc.read      then 0x4 else 0;
+let w : UInt32 := if acc.write     then 0x2 else 0;
+let x : UInt32 := if acc.execution then 0x1 else 0;
+r.lor $ w.lor x
+
+structure FileRight :=
+(user group other : AccessRight := { })
+
+def FileRight.flags (acc : FileRight) : UInt32 :=
+let u : UInt32 := acc.user.flags.shiftLeft 6;
+let g : UInt32 := acc.group.flags.shiftLeft 3;
+let o : UInt32 := acc.other.flags;
+u.lor $ g.lor o
+
+namespace Access
+
+@[extern "lean_chmod"]
+constant Prim.setAccessRights (filename : @& String) (mode : UInt32) : IO Unit :=
+arbitrary _
+
+def setAccessRights (filename : String) (mode : FileRight) : IO Unit :=
+Prim.setAccessRights filename mode.flags
+
+end Access
 
 /- References -/
 constant RefPointed (α : Type) : PointedType := arbitrary _
diff --git a/src/Init/System/IOError.lean b/src/Init/System/IOError.lean
new file mode 100644
index 0000000000..c647b651d6
--- /dev/null
+++ b/src/Init/System/IOError.lean
@@ -0,0 +1,193 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Simon Hudon
+-/
+
+prelude
+import Init.Core
+import Init.Data.UInt
+import Init.Data.ToString
+import Init.Data.String.Basic
+
+/-
+Immitate the structure of IOErrorType in Haskell:
+https://hackage.haskell.org/package/base-4.12.0.0/docs/System-IO-Error.html#t:IOErrorType
+-/
+inductive IO.Error
+| alreadyExists (details : String) -- EEXIST, EINPROGRESS, EISCONN
+| otherError (details : String)    -- EFAULT, default
+| resourceBusy (details : String)
+    -- EADDRINUSE, EBUSY, EDEADLK, ETXTBSY
+| resourceVanished (details : String)
+    -- ECONNRESET, EIDRM, ENETDOWN, ENETRESET,
+    -- ENOLINK, EPIPE
+| unsupportedOperation (details : String)
+    -- EADDRNOTAVAIL, EAFNOSUPPORT, ENODEV, ENOPROTOOPT
+    -- ENOSYS, EOPNOTSUPP, ERANGE, ESPIPE, EXDEV
+| hardwareFault (details : String)          -- EIO
+| unsatisfiedConstraints (details : String) -- ENOTEMPTY
+| illegalOperation (details : String)       -- ENOTTY
+| protocolError (details : String)
+    -- EPROTO, EPROTONOSUPPORT, EPROTOTYPE
+| timeExpired (details : String)
+    -- ETIME, ETIMEDOUT
+
+| interrupted (filename : String) (details : String)       -- EINTR
+| noFileOrDirectory (filename : String) (details : String) -- ENOENT
+| invalidArgument (filename : Option String) (details : String)
+    -- ELOOP, ENAMETOOLONG, EDESTADDRREQ, EILSEQ, EINVAL, EDOM, EBADF
+    -- ENOEXEC, ENOSTR, ENOTCONN, ENOTSOCK
+| permissionDenied (filename : Option String) (details : String)
+    -- EACCES, EROFS, ECONNABORTED, EFBIG, EPERM
+| resourceExhausted (filename : Option String) (details : String)
+    -- EMFILE, ENFILE, ENOSPC, E2BIG, EAGAIN, EMLINK:
+    -- EMSGSIZE, ENOBUFS, ENOLCK, ENOMEM, ENOSR:
+| inappropriateType (filename : Option String) (details : String)
+    -- EISDIR, EBADMSG, ENOTDIR:
+| noSuchThing (filename : Option String) (details : String)
+    -- ENXIO, EHOSTUNREACH, ENETUNREACH, ECHILD, ECONNREFUSED,
+    -- ENODATA, ENOMSG, ESRCH
+-- overflow -- EOVERFLOW
+
+| unexpectedEof
+| userError (msg : String)
+
+@[export mk_io_user_error]
+def IO.userError (s : String) : IO.Error :=
+IO.Error.userError s
+
+namespace IO.Error
+
+@[export lean_mk_io_error_eof]
+def mkEofError : IO.Error := unexpectedEof
+
+@[export lean_mk_io_error_inappropriate_type_file]
+def mkInappropriateTypeFile : String → String → IO.Error :=
+inappropriateType ∘ some
+
+@[export lean_mk_io_error_interrupted]
+def mkInterrupted : String → String → IO.Error :=
+interrupted
+
+@[export lean_mk_io_error_invalid_argument_file]
+def mkInvalidArgumentFile : String → String → IO.Error :=
+invalidArgument ∘ some
+
+@[export lean_mk_io_error_no_file_or_directory]
+def mkNoFileOrDirectory : String → String → IO.Error :=
+noFileOrDirectory
+
+@[export lean_mk_io_error_no_such_thing_file]
+def mkNoSuchThingFile : String → String → IO.Error :=
+noSuchThing ∘ some
+
+@[export lean_mk_io_error_permission_denied_file]
+def mkPermissionDeniedFile : String → String → IO.Error :=
+permissionDenied ∘ some
+
+@[export lean_mk_io_error_resource_exhausted_file]
+def mkResourceExhaustedFile : String → String → IO.Error :=
+resourceExhausted ∘ some
+
+@[export lean_mk_io_error_unsupported_operation]
+def mkUnsupportedOperation : String → IO.Error :=
+unsupportedOperation
+
+@[export lean_mk_io_error_resource_exhausted]
+def mkResourceExhausted : String → IO.Error :=
+resourceExhausted none
+
+@[export lean_mk_io_error_already_exists]
+def mkAlreadyExists : String → IO.Error :=
+alreadyExists
+
+@[export lean_mk_io_error_inappropriate_type]
+def mkInappropriateType : String → IO.Error :=
+inappropriateType none
+
+@[export lean_mk_io_error_no_such_thing]
+def mkNoSuchThing : String → IO.Error :=
+noSuchThing none
+
+@[export lean_mk_io_error_resource_vanished]
+def mkResourceVanished : String → IO.Error :=
+resourceVanished
+
+@[export lean_mk_io_error_resource_busy]
+def mkResourceBusy : String → IO.Error :=
+resourceBusy
+
+@[export lean_mk_io_error_invalid_argument]
+def mkInvalidArgument : String → IO.Error :=
+invalidArgument none
+
+@[export lean_mk_io_error_other_error]
+def mkOtherError : String → IO.Error :=
+otherError
+
+@[export lean_mk_io_error_permission_denied]
+def mkPermissionDenied : String → IO.Error :=
+permissionDenied none
+
+@[export lean_mk_io_error_hardware_fault]
+def mkHardwareFault : String → IO.Error :=
+hardwareFault
+
+@[export lean_mk_io_error_unsatisfied_constraints]
+def mkUnsatisfiedConstraints : String → IO.Error :=
+unsatisfiedConstraints
+
+@[export lean_mk_io_error_illegal_operation]
+def mkIllegalOperation : String → IO.Error :=
+illegalOperation
+
+@[export lean_mk_io_error_protocol_error]
+def mkProtocolError : String → IO.Error :=
+protocolError
+
+@[export lean_mk_io_error_time_expired]
+def mkTimeExpired : String → IO.Error :=
+timeExpired
+
+private def downCaseFirst (s : String) : String := s.set 0 (s.get 0).toLower
+
+def fopenErrorToString (gist fn : String) : Option String → String
+| some details => gist ++ ": " ++ downCaseFirst details ++ "\n  file: " ++ fn
+| none => gist ++ "\n  file: " ++ fn
+
+def otherErrorToString (gist : String) : Option String → String
+| some details => gist ++ ": " ++ downCaseFirst details
+| none => gist
+
+@[export lean_io_error_to_string]
+def toString : IO.Error → String
+| unexpectedEof                       => "End of file"
+| inappropriateType (some fn) details => fopenErrorToString "Inappropriate type" fn details
+| inappropriateType none details      => otherErrorToString "Inappropriate type" details
+| interrupted fn details              => fopenErrorToString "Interrupted system call" fn details
+| invalidArgument (some fn) details   => fopenErrorToString "Invalid argument" fn details
+| invalidArgument none details        => otherErrorToString "Invalid argument" details
+| noFileOrDirectory fn details        => fopenErrorToString "No such file or directory" fn none
+| noSuchThing (some fn) details       => fopenErrorToString "No such thing" fn details
+| noSuchThing none details            => otherErrorToString "No such thing" details
+| permissionDenied (some fn) details  => fopenErrorToString details fn none
+| permissionDenied none details       => otherErrorToString details none
+| resourceExhausted (some fn) details => fopenErrorToString "Resource exhausted" fn details
+| resourceExhausted none details      => otherErrorToString "Resource exhausted" details
+| alreadyExists details               => otherErrorToString "Already exists" details
+| otherError details                  => details
+| resourceBusy details                => otherErrorToString "Resource busy" details
+| resourceVanished details            => otherErrorToString "Resource vanished" details
+| hardwareFault _                     => otherErrorToString "Hardware fault" none
+| illegalOperation details            => otherErrorToString "Illegal operation" details
+| protocolError details               => otherErrorToString "Protocol error" details
+| timeExpired details                 => otherErrorToString "Time expired" details
+| unsatisfiedConstraints details      => otherErrorToString "Directory not empty" none
+| unsupportedOperation details        => otherErrorToString "Unsupported operation" details
+| userError msg                       => msg
+
+instance : HasToString IO.Error := ⟨ IO.Error.toString ⟩
+instance : Inhabited IO.Error := ⟨ userError "" ⟩
+
+end IO.Error
diff --git a/src/cmake/check_main.sh b/src/cmake/check_main.sh
new file mode 100644
index 0000000000..ad69f829e6
--- /dev/null
+++ b/src/cmake/check_main.sh
@@ -0,0 +1,69 @@
+#!/usr/bin/env bash
+
+set -e
+
+if [ $# -ne 3 -a $# -ne 2 ]; then
+    echo "Usage: test_single.sh [lean-executable-path] [file] [yes/no]?"
+    exit 1
+fi
+ulimit -s 8192
+LEAN=$1
+BIN_DIR=../../../bin
+export LEAN_PATH=Init=../../../src/Init:Test=.
+
+if [ $# -ne 3 ]; then
+    INTERACTIVE=no
+else
+    INTERACTIVE=$3
+fi
+ff=$2
+
+if [[ "$OSTYPE" == "msys" ]]; then
+    # Windows running MSYS2
+    # Replace /c/ with c:, and / with \\
+    ff=$(echo $ff  | sed 's|^/\([a-z]\)/|\1:/|' | sed 's|/|\\\\|g')
+fi
+
+DIFF=diff
+if diff --color --help >/dev/null 2>&1; then
+  DIFF="diff --color";
+fi
+
+$LEAN --cpp="$ff".cpp "$ff" || echo oh ho!
+if [ $? -ne 0 ]; then
+    echo "Failed to compile $ff into C++ file"
+    exit 1
+fi
+
+$BIN_DIR/leanc -O3 -DNDEBUG -o "$ff.out" $ff.cpp
+if [ $? -ne 0 ]; then
+    echo "Failed to compile C++ file $ff.cpp"
+    exit 1
+fi
+"./$ff.out" > "$ff.produced.out" 2>&1 || true
+
+if test -f "$ff.expected.out"; then
+    if $DIFF -u --ignore-all-space -I "executing external script" "$ff.expected.out" "$ff.produced.out"; then
+        echo "-- checked"
+        exit 0
+    else
+        echo "ERROR: file $ff.produced.out does not match $ff.expected.out"
+        if [ $INTERACTIVE == "yes" ]; then
+            meld "$ff.produced.out" "$ff.expected.out"
+            if diff -I "executing external script" "$ff.expected.out" "$ff.produced.out"; then
+                echo "-- mismatch was fixed"
+            fi
+        fi
+        exit 1
+    fi
+else
+    echo "ERROR: file $ff.expected.out does not exist"
+    if [ $INTERACTIVE == "yes" ]; then
+        read -p "copy $ff.produced.out (y/n)? "
+        if [ $REPLY == "y" ]; then
+            cp -- "$ff.produced.out" "$ff.expected.out"
+            echo "-- copied $ff.produced.out --> $ff.expected.out"
+        fi
+    fi
+    exit 1
+fi
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 291a9ae743..3b31593497 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "runtime/sstream.h"
 #include "runtime/compact.h"
 #include "util/timeit.h"
+#include "util/io.h"
 #include "util/option_declarations.h"
 #include "kernel/replace_fn.h"
 #include "kernel/find_fn.h"
@@ -403,8 +404,12 @@ static environment eval_cmd(parser & p) {
     out.report();
     if (io_result_is_error(r.raw())) {
         message_builder msg = p.mk_message(p.cmd_pos(), p.pos(), ERROR);
-        msg << string_to_std(io_result_get_error(r.raw()));
+        object * err = io_result_get_error(r.raw());
+        inc_ref(err);
+        object * str = lean_io_error_to_string(err);
+        msg << string_to_std(str);
         msg.report();
+        dec_ref(str);
     }
     return p.env();
 }
diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index 537450794b..3a67db48e4 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -21,6 +21,8 @@ Author: Leonardo de Moura
 #include <cstdlib>
 #include <cctype>
 #include <sys/stat.h>
+#include "util/io.h"
+#include "runtime/utf8.h"
 #include "runtime/object.h"
 #include "runtime/thread.h"
 #include "runtime/allocprof.h"
@@ -32,8 +34,41 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
+
+extern "C" lean_object* lean_mk_io_error_permission_denied_file(lean_object*, lean_object*);
+extern "C" lean_object* lean_mk_io_error_no_file_or_directory(lean_object*, lean_object*);
+extern "C" lean_object* mk_io_user_error(lean_object*);
+extern "C" lean_object* lean_string_append(lean_object*, lean_object*);
+extern "C" lean_object* lean_mk_io_error_resource_exhausted_file(lean_object*, lean_object*);
+extern "C" lean_object* lean_mk_io_error_interrupted(lean_object*, lean_object*);
+extern "C" lean_object* lean_mk_io_error_invalid_argument_file(lean_object*, lean_object*);
+extern "C" lean_object* lean_mk_io_error_no_such_thing_file(lean_object*, lean_object*);
+extern "C" lean_object* lean_mk_io_error_inappropriate_type_file(lean_object*, lean_object*);
+extern "C" lean_object* lean_mk_io_error_eof();
+extern "C" lean_object* lean_mk_io_error_unsupported_operation(lean_object*);
+extern "C" lean_object* lean_mk_io_error_resource_exhausted(lean_object*);
+extern "C" lean_object* lean_mk_io_error_already_exists(lean_object*);
+extern "C" lean_object* lean_mk_io_error_inappropriate_type(lean_object*);
+extern "C" lean_object* lean_mk_io_error_no_such_thing(lean_object*);
+extern "C" lean_object* lean_mk_io_error_resource_vanished(lean_object*);
+extern "C" lean_object* lean_mk_io_error_resource_busy(lean_object*);
+extern "C" lean_object* lean_mk_io_error_invalid_argument(lean_object*);
+extern "C" lean_object* lean_mk_io_error_other_error(lean_object*);
+extern "C" lean_object* lean_mk_io_error_permission_denied(lean_object*);
+extern "C" lean_object* lean_mk_io_error_no_such_thing(lean_object*);
+extern "C" lean_object* lean_mk_io_error_unsupported_operation(lean_object*);
+extern "C" lean_object* lean_mk_io_error_hardware_fault(lean_object*);
+extern "C" lean_object* lean_mk_io_error_unsatisfied_constraints(lean_object*);
+extern "C" lean_object* lean_mk_io_error_illegal_operation(lean_object*);
+extern "C" lean_object* lean_mk_io_error_protocol_error(lean_object*);
+extern "C" lean_object* lean_mk_io_error_time_expired(lean_object*);
+
 extern "C" void lean_io_result_show_error(b_obj_arg r) {
-    std::cerr << "uncaught exception: " << string_cstr(io_result_get_error(r)) << std::endl;
+    object * err = io_result_get_error(r);
+    inc_ref(err);
+    object * str = lean_io_error_to_string(err);
+    std::cerr << "uncaught exception: " << string_cstr(str) << std::endl;
+    dec_ref(str);
 }
 
 obj_res set_io_result(obj_arg a) {
@@ -50,10 +85,7 @@ obj_res set_io_error(obj_arg e) {
     return new_r;
 }
 
-object * mk_io_user_error(object * str) {
-    // TODO(Leo): fix after we expand IO.Error
-    return str;
-}
+extern "C" object * mk_io_user_error(object * str);
 
 obj_res set_io_error(char const * msg) {
     return set_io_error(mk_io_user_error(mk_string(msg)));
@@ -102,37 +134,258 @@ extern "C" obj_res lean_io_prim_get_line(obj_arg /* w */) {
     lean_unreachable();
 }
 
-/* handle.mk (s : string) (m : mode) (bin : bool := ff) : eio handle */
-extern "C" obj_res lean_io_prim_handle_mk(b_obj_arg /* s */, uint8 /* mode */, uint8 /* bin */, obj_arg /* w */) {
-    // not implemented yet
-    lean_unreachable();
+static lean_external_class * g_io_handle_external_class = nullptr;
+
+static void io_handle_finalizer(void * h) {
+    fclose(static_cast<FILE *>(h));
 }
 
-/* handle.is_eof : handle → eio bool */
-extern "C" obj_res lean_io_prim_handle_is_eof(b_obj_arg /* h */, obj_arg /* w */) {
-    // not implemented yet
-    lean_unreachable();
+static void io_handle_foreach(void * /* mod */, b_obj_arg /* fn */) {
 }
 
-/* handle.flush : handle → eio bool */
-extern "C" obj_res lean_io_prim_handle_flush(b_obj_arg /* h */, obj_arg /* w */) {
-    // not implemented yet
-    lean_unreachable();
+static lean_object * io_wrap_handle(FILE *hfile) {
+    return lean_alloc_external(g_io_handle_external_class, hfile);
 }
 
-/* handle.close : handle → eio unit */
-extern "C" obj_res lean_io_prim_handle_close(b_obj_arg /* h */, obj_arg /* w */) {
-    // not implemented yet
-    lean_unreachable();
+static FILE * io_get_handle(lean_object * hfile) {
+    return static_cast<FILE *>(lean_get_external_data(hfile));
 }
 
-/* handle.get_line : handle → eio unit */
-extern "C" obj_res lean_io_prim_handle_get_line(b_obj_arg /* h */, obj_arg /* w */) {
-    // not implemented yet
-    lean_unreachable();
+obj_res decode_io_error(int errnum, b_obj_arg fname) {
+    object * details = mk_string(strerror(errnum));
+    switch (errnum) {
+    case EINTR:
+        lean_assert(fname != nullptr);
+        inc_ref(fname);
+        return lean_mk_io_error_interrupted(fname, details);
+    case ELOOP: case ENAMETOOLONG: case EDESTADDRREQ:
+    case EBADF: case EDOM: case EINVAL: case EILSEQ:
+    case ENOEXEC: case ENOSTR: case ENOTCONN:
+    case ENOTSOCK:
+        if (fname == nullptr) {
+            return lean_mk_io_error_invalid_argument(details);
+        } else {
+            inc_ref(fname);
+            return lean_mk_io_error_invalid_argument_file(fname, details);
+        }
+    case ENOENT:
+        lean_assert(fname != nullptr);
+        inc_ref(fname);
+        return lean_mk_io_error_no_file_or_directory(fname, details);
+    case EACCES: case EROFS: case ECONNABORTED: case EFBIG:
+    case EPERM:
+        if (fname == nullptr) {
+            return lean_mk_io_error_permission_denied(details);
+        } else {
+            inc_ref(fname);
+            return lean_mk_io_error_permission_denied_file(fname, details);
+        }
+    case EMFILE: case ENFILE: case ENOSPC:
+    case E2BIG:  case EAGAIN: case EMLINK:
+    case EMSGSIZE: case ENOBUFS: case ENOLCK:
+    case ENOMEM: case ENOSR:
+        if (fname == nullptr) {
+            return lean_mk_io_error_resource_exhausted(details);
+        } else {
+            inc_ref(fname);
+            return lean_mk_io_error_resource_exhausted_file(fname, details);
+        }
+    case EISDIR: case EBADMSG: case ENOTDIR:
+        if (fname == nullptr) {
+            return lean_mk_io_error_inappropriate_type(details);
+        } else {
+            inc_ref(fname);
+            return lean_mk_io_error_inappropriate_type_file(fname, details);
+        }
+    case ENXIO: case EHOSTUNREACH: case ENETUNREACH:
+    case ECHILD: case ECONNREFUSED: case ENODATA:
+    case ENOMSG: case ESRCH:
+        if (fname == nullptr) {
+            return lean_mk_io_error_no_such_thing(details);
+        } else {
+            inc_ref(fname);
+            return lean_mk_io_error_no_such_thing_file(fname, details);
+        }
+    case EEXIST: case EINPROGRESS: case EISCONN:
+        lean_assert(fname == nullptr);
+        return lean_mk_io_error_already_exists(details);
+    case EIO:
+        lean_assert(fname == nullptr);
+        return lean_mk_io_error_hardware_fault(details);
+    case ENOTEMPTY:
+        lean_assert(fname == nullptr);
+        return lean_mk_io_error_unsatisfied_constraints(details);
+    case ENOTTY:
+        lean_assert(fname == nullptr);
+        return lean_mk_io_error_illegal_operation(details);
+    case ECONNRESET: case EIDRM: case ENETDOWN: case ENETRESET:
+    case ENOLINK: case EPIPE:
+        lean_assert(fname == nullptr);
+        return lean_mk_io_error_resource_vanished(details);
+    case EPROTO: case EPROTONOSUPPORT: case EPROTOTYPE:
+        lean_assert(fname == nullptr);
+        return lean_mk_io_error_protocol_error(details);
+    case ETIME: case ETIMEDOUT:
+        lean_assert(fname == nullptr);
+        return lean_mk_io_error_time_expired(details);
+    case EADDRINUSE: case EBUSY: case EDEADLK: case ETXTBSY:
+        lean_assert(fname == nullptr);
+        return lean_mk_io_error_resource_busy(details);
+    case EADDRNOTAVAIL: case EAFNOSUPPORT: case ENODEV:
+    case ENOPROTOOPT: case ENOSYS: case EOPNOTSUPP:
+    case ERANGE: case ESPIPE: case EXDEV:
+        lean_assert(fname == nullptr);
+        return lean_mk_io_error_unsupported_operation(details);
+    case EFAULT:
+    default:
+        lean_assert(fname == nullptr);
+        return lean_mk_io_error_other_error(details);
+    }
 }
 
-/* timeit {α : Type} (msg : @& string) (fn : io α) : io α */
+/* IO.setAccessRights (filename : @& String) (mode : UInt32) : IO Handle */
+extern "C" obj_res lean_chmod (b_obj_arg filename, uint32_t mode, obj_arg /* w */) {
+    if (!chmod(lean_string_cstr(filename), mode)) {
+        return set_io_result(box(0));
+    } else {
+        return set_io_error(decode_io_error(errno, filename));
+    }
+}
+
+/* Handle.mk (filename : @& String) (mode : @& String) : IO Handle */
+extern "C" obj_res lean_io_prim_handle_mk(b_obj_arg filename, b_obj_arg modeStr, obj_arg /* w */) {
+    FILE *fp = fopen(lean_string_cstr(filename), lean_string_cstr(modeStr));
+    if (!fp) {
+        return set_io_error(decode_io_error(errno, filename));
+    } else {
+        return set_io_result(io_wrap_handle(fp));
+    }
+}
+
+/* Handle.isEof : (@& Handle) → IO Bool */
+extern "C" obj_res lean_io_prim_handle_is_eof(b_obj_arg h, obj_arg /* w */) {
+    FILE * fp = io_get_handle(h);
+    return set_io_result(box(std::feof(fp) != 0));
+}
+
+/* Handle.flush : (@& Handle) → IO Bool */
+extern "C" obj_res lean_io_prim_handle_flush(b_obj_arg h, obj_arg /* w */) {
+    FILE * fp = io_get_handle(h);
+    if (!std::fflush(fp)) {
+        return set_io_result(box(0));
+    } else {
+        return set_io_error(decode_io_error(errno, nullptr));
+    }
+}
+
+/* Handle.readByte : (@& Handle) → IO UInt8 */
+extern "C" obj_res lean_io_prim_handle_read_byte(b_obj_arg h, obj_arg /* w */) {
+    FILE * fp = io_get_handle(h);
+    int c = std::fgetc(fp);
+    if (c != EOF) {
+        return set_io_result(box(c));
+    } else {
+        return set_io_error(decode_io_error(errno, nullptr));
+    }
+}
+
+/* Handle.writeByte : (@& Handle) → UInt8 → IO unit */
+extern "C" obj_res lean_io_prim_handle_write_byte(b_obj_arg h, uint8 c, obj_arg /* w */) {
+    FILE * fp = io_get_handle(h);
+    if (std::fputc(c, fp) != EOF) {
+        return set_io_result(box(0));
+    } else {
+        return set_io_error(decode_io_error(errno, nullptr));
+    }
+}
+
+/* Handle.read : (@& Handle) → USize → IO ByteArray */
+extern "C" obj_res lean_io_prim_handle_read(b_obj_arg h, usize nbytes, obj_arg /* w */) {
+    FILE * fp = io_get_handle(h);
+    if (feof(fp)) {
+        return set_io_error(lean_mk_io_error_eof());
+    }
+    obj_res res = lean_alloc_sarray(1, 0, nbytes);
+    usize n = std::fread(lean_sarray_cptr(res), 1, nbytes, fp);
+    if (n > 0) {
+        lean_sarray_set_size(res, n);
+        return set_io_result(res);
+    } else if (feof(fp)) {
+        dec_ref(res);
+        return set_io_result(alloc_sarray(1, 0, 0));
+    } else {
+        dec_ref(res);
+        return set_io_error(decode_io_error(errno, nullptr));
+    }
+}
+
+/* Handle.write : (@& Handle) → (@& ByteArray) → IO unit */
+extern "C" obj_res lean_io_prim_handle_write(b_obj_arg h, b_obj_arg buf, obj_arg /* w */) {
+    FILE * fp = io_get_handle(h);
+    usize n = lean_sarray_size(buf);
+    usize m = std::fwrite(lean_sarray_cptr(buf), 1, n, fp);
+    if (m == n) {
+        return set_io_result(box(0));
+    } else {
+        return set_io_error(decode_io_error(errno, nullptr));
+    }
+}
+
+obj_res lean_get_line(FILE * fp) {
+    const int buf_sz = 64;
+    lean_string_object * buf_str = lean_to_string(lean_alloc_string(0, buf_sz, 0));
+    lean_object * res_str        = lean_alloc_string(1, buf_sz, 0);
+    lean_to_string(res_str)->m_data[0] = '\0';
+    char * out = nullptr;
+    do {
+        out = std::fgets(buf_str->m_data, buf_sz, fp);
+        if (out != nullptr) {
+            buf_str->m_size   = strlen(buf_str->m_data);
+            buf_str->m_length = buf_str->m_size;
+            buf_str->m_size++;
+            res_str = lean_string_append(res_str, reinterpret_cast<object *>(buf_str));
+        }
+    } while (out != nullptr && buf_str->m_size == buf_sz);
+    dec_ref(reinterpret_cast<object *>(buf_str));
+    lean_to_string(res_str)->m_length = utf8_strlen(lean_to_string(res_str)->m_data);
+    if (out == nullptr && !feof(fp)) {
+        dec_ref(res_str);
+        return nullptr;
+    } else {
+        return res_str;
+    }
+}
+
+/* Handle.getLine : (@& Handle) → IO Unit                     */
+/*   The line returned by `lean_io_prim_handle_get_line` */
+/*   is truncated at the first '\0' character and the    */
+/*   rest of the line is discarded.                      */
+extern "C" obj_res lean_io_prim_handle_get_line(b_obj_arg h, obj_arg /* w */) {
+    FILE * fp = io_get_handle(h);
+    if (feof(fp)) {
+        return set_io_error(lean_mk_io_error_eof());
+    }
+    object * res = lean_get_line(fp);
+    if (res != nullptr) {
+        return set_io_result(res);
+    } else if (feof(fp)) {
+        return set_io_result(lean_mk_string(""));
+    } else {
+        return set_io_error(decode_io_error(errno, nullptr));
+    }
+}
+
+/* Handle.putStr : (@& Handle) → (@& String) → IO Unit */
+extern "C" obj_res lean_io_prim_handle_put_str(b_obj_arg h, b_obj_arg s, obj_arg /* w */) {
+    FILE * fp = io_get_handle(h);
+    if (std::fputs(lean_string_cstr(s), fp) != EOF) {
+        return set_io_result(box(0));
+    } else {
+        return set_io_error(decode_io_error(errno, nullptr));
+    }
+}
+
+/* timeit {α : Type} (msg : @& String) (fn : IO α) : IO α */
 extern "C" obj_res lean_io_timeit(b_obj_arg msg, obj_arg fn, obj_arg w) {
     auto start = std::chrono::steady_clock::now();
     w = apply_1(fn, w);
@@ -148,7 +401,7 @@ extern "C" obj_res lean_io_timeit(b_obj_arg msg, obj_arg fn, obj_arg w) {
     return w;
 }
 
-/* allocprof {α : Type} (msg : string) (fn : io α) : io α */
+/* allocprof {α : Type} (msg : @& String) (fn : IO α) : IO α */
 extern "C" obj_res lean_io_allocprof(b_obj_arg msg, obj_arg fn, obj_arg w) {
     std::ostream & out = std::cerr; // TODO(Leo): replace?
     allocprof prof(out, string_cstr(msg));
@@ -363,6 +616,7 @@ extern "C" obj_res lean_io_ref_ptr_eq(b_obj_arg ref1, b_obj_arg ref2, obj_arg) {
 void initialize_io() {
     g_io_error_nullptr_read = mk_string("null reference read");
     mark_persistent(g_io_error_nullptr_read);
+    g_io_handle_external_class = lean_register_external_class(io_handle_finalizer, io_handle_foreach);
 }
 
 void finalize_io() {
diff --git a/src/runtime/lean.h b/src/runtime/lean.h
index c8f0c1b76f..8f21e3a549 100644
--- a/src/runtime/lean.h
+++ b/src/runtime/lean.h
@@ -177,7 +177,7 @@ typedef struct {
 
 typedef struct {
     lean_object m_header;
-    size_t      m_size;
+    size_t      m_size;     /* byte length including '\0' terminator */
     size_t      m_capacity;
     size_t      m_length;   /* UTF8 length */
     char        m_data[0];
@@ -951,6 +951,15 @@ static inline lean_obj_res lean_byte_array_size(b_lean_obj_arg a) {
     return lean_box(lean_sarray_size(a));
 }
 
+/* static inline uint8_t lean_byte_array_uget(b_lean_obj_arg a, size_t i) { */
+/*     assert(i < lean_sarray_size(a)); */
+/*     return lean_to_sarray(a)->m_data[i]; */
+/* } */
+
+/* static inline uint8_t lean_byte_array_fget(b_lean_obj_arg a, b_lean_obj_arg i) { */
+/*     return lean_byte_array_uget(a, lean_unbox(i)); */
+/* } */
+
 static inline uint8_t lean_byte_array_get(b_lean_obj_arg a, b_lean_obj_arg i) {
     if (lean_is_scalar(i)) {
         size_t idx = lean_unbox(i);
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 6b571939aa..9e1e1edba1 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -143,6 +143,9 @@ add_test(lean_ghash2   "${CMAKE_CURRENT_BINARY_DIR}/lean" --githash)
 # add_test(lean_new_frontend "${LEAN_SOURCE_DIR}/../bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/Init/Core.lean")
 add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "-z")
 add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean")
+add_test(NAME lean_test_main_error
+         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run"
+         COMMAND bash "${LEAN_SOURCE_DIR}/cmake/check_main.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "print_error.lean")
 if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
   # The following test cannot be executed on Windows because of the
   # bash script timeout.sh
diff --git a/tests/bench/parser.lean b/tests/bench/parser.lean
index 5d5a5561e2..38c16f5d0f 100644
--- a/tests/bench/parser.lean
+++ b/tests/bench/parser.lean
@@ -6,4 +6,4 @@ def main : List String → IO Unit
   n.toNat.forM $ fun _ =>
     Lean.Parser.parseFile env fname *> pure ();
   pure ()
-| _    => throw "give file"
+| _    => throw $ IO.userError "give file"
diff --git a/tests/bench/rbmap_checkpoint.lean b/tests/bench/rbmap_checkpoint.lean
index 4a4e314063..5733c85cc0 100644
--- a/tests/bench/rbmap_checkpoint.lean
+++ b/tests/bench/rbmap_checkpoint.lean
@@ -82,9 +82,8 @@ def myLen : List Tree → Nat → Nat
 | _ :: xs,   r => myLen xs r
 | [], r => r
 
-def main (xs : List String) : IO UInt32 :=
-do
-[n, freq] ← pure xs | throw "invalid input";
+def main (xs : List String) : IO UInt32 := do
+[n, freq] ← pure xs | throw $ IO.userError "invalid input";
 let n     := n.toNat;
 let freq  := freq.toNat;
 let freq  := if freq == 0 then 1 else freq;
diff --git a/tests/lean/eval_except.lean b/tests/lean/eval_except.lean
new file mode 100644
index 0000000000..b104a63a21
--- /dev/null
+++ b/tests/lean/eval_except.lean
@@ -0,0 +1,5 @@
+prelude
+import Init.System.IO
+
+#eval (throw $ IO.userError "this is my error" : IO Unit)
+#eval (throw $ IO.Error.noFileOrDirectory "file.ext" "and details" : IO Unit)
diff --git a/tests/lean/eval_except.lean.expected.out b/tests/lean/eval_except.lean.expected.out
new file mode 100644
index 0000000000..5e474947d4
--- /dev/null
+++ b/tests/lean/eval_except.lean.expected.out
@@ -0,0 +1,5 @@
+
+eval_except.lean:4:0: error: this is my error
+
+eval_except.lean:5:0: error: No such file or directory
+  file: file.ext
diff --git a/tests/lean/file_not_found.lean b/tests/lean/file_not_found.lean
new file mode 100644
index 0000000000..5d75ca9a4b
--- /dev/null
+++ b/tests/lean/file_not_found.lean
@@ -0,0 +1,16 @@
+prelude
+import Init.System.IO
+
+open IO.FS
+
+#eval (IO.FS.Handle.mk "non-existant-file.txt" Mode.read *> pure () : IO Unit)
+#eval do condM (IO.fileExists "readonly.txt")
+               (pure ())
+               (IO.FS.withFile "readonly.txt" Mode.write $ fun _ => pure ());
+         IO.Access.setAccessRights "readonly.txt" { user := { read := true } };
+         (pure () : IO Unit)
+#eval (IO.FS.Handle.mk "readonly.txt" Mode.write *> pure () : IO Unit)
+#eval do h ← IO.FS.Handle.mk "readonly.txt" Mode.read;
+         h.putStr "foo";
+         IO.println "foo";
+         (pure () : IO Unit)
diff --git a/tests/lean/file_not_found.lean.expected.out b/tests/lean/file_not_found.lean.expected.out
new file mode 100644
index 0000000000..0909115fc1
--- /dev/null
+++ b/tests/lean/file_not_found.lean.expected.out
@@ -0,0 +1,9 @@
+
+file_not_found.lean:6:0: error: No such file or directory
+  file: non-existant-file.txt
+
+
+file_not_found.lean:12:0: error: Permission denied
+  file: readonly.txt
+
+file_not_found.lean:13:0: error: Invalid argument: bad file descriptor
diff --git a/tests/lean/mvar1.lean b/tests/lean/mvar1.lean
index 85f9ec40dc..56aa57c5e4 100644
--- a/tests/lean/mvar1.lean
+++ b/tests/lean/mvar1.lean
@@ -2,7 +2,7 @@ import Init.Lean.MetavarContext
 open Lean
 
 def check (b : Bool) : IO Unit :=
-unless b (throw "error")
+unless b (throw $ IO.userError "error")
 
 def f := mkConst `f []
 def g := mkConst `g []
diff --git a/tests/lean/mvar2.lean b/tests/lean/mvar2.lean
index 77a6bdbd1b..3bae591d80 100644
--- a/tests/lean/mvar2.lean
+++ b/tests/lean/mvar2.lean
@@ -2,7 +2,7 @@ import Init.Lean.MetavarContext
 open Lean
 
 def check (b : Bool) : IO Unit :=
-unless b (throw "error")
+unless b (throw $ IO.userError "error")
 
 def f := mkConst `f []
 def g := mkConst `g []
diff --git a/tests/lean/mvar3.lean b/tests/lean/mvar3.lean
index c8ddc49c4b..a5494cf603 100644
--- a/tests/lean/mvar3.lean
+++ b/tests/lean/mvar3.lean
@@ -8,7 +8,7 @@ match MetavarContext.mkLambda xs e lctx { mctx := mctx, ngen := ngen } with
 | EStateM.Result.error e s => Except.error e
 
 def check (b : Bool) : IO Unit :=
-unless b (throw "error")
+unless b (throw $ IO.userError "error")
 
 def f := mkConst `f
 def g := mkConst `g
diff --git a/tests/lean/run/IO_test.lean b/tests/lean/run/IO_test.lean
new file mode 100644
index 0000000000..9920d65ba0
--- /dev/null
+++ b/tests/lean/run/IO_test.lean
@@ -0,0 +1,82 @@
+prelude
+import Init.System.IO
+import Init.Data.List.Control
+
+open IO.FS
+
+instance : HasRepr UInt8 := ⟨ toString ⟩
+
+def check_eq {α} [HasBeq α] [HasRepr α] (tag : String) (expected actual : α) : IO Unit :=
+unless (expected == actual) $ throw $ IO.userError $
+  "assertion failure \"" ++ tag ++
+    "\":\n  expected: " ++ repr expected ++
+       "\n  actual:   " ++ repr actual
+
+def test : IO Unit := do
+let xs : ByteArray := ⟨#[1,2,3,4]⟩;
+let fn := "foo.txt";
+withFile fn Mode.write $ fun h => do
+{ h.write xs;
+  h.write xs;
+  pure () };
+ys ← withFile "foo.txt" Mode.read $ fun h => h.read 10;
+check_eq "1" (xs.toList ++ xs.toList) ys.toList;
+withFile fn Mode.append $ fun h => do
+{ h.write ⟨#[5,6,7,8]⟩;
+  pure () };
+withFile "foo.txt" Mode.read $ fun h => do
+  { ys ← h.read 10;
+    check_eq "2" [1,2,3,4,1,2,3,4,5,6] ys.toList;
+    ys ← h.read 2;
+    check_eq "3" [7,8] ys.toList;
+    b ← h.isEof;
+    unless (!b)
+      (throw $ IO.userError $ "wrong (4): ");
+    ys ← h.read 2;
+    check_eq "5" [] ys.toList;
+    b ← h.isEof;
+    unless b
+      (throw $ IO.userError $ "wrong (6): ") };
+pure ()
+
+#eval test
+
+def test2 : IO Unit := do
+let fn2 := "foo2.txt";
+let xs₀ : String := "⟨[₂,α]⟩";
+let xs₁ := "⟨[6,8,@]⟩";
+let xs₂ := "/* Handle.getLine : Handle → IO Unit                     */" ++
+           "/*   The line returned by `lean_io_prim_handle_get_line` */" ++
+           "/*   is truncated at the first \'\\0\' character and the    */" ++
+           "/*   rest of the line is discarded.                      */";
+    -- multi-buffer line
+withFile fn2 Mode.write $ fun h => pure ();
+
+withFile fn2 Mode.write $ fun h => do
+{ h.putStr xs₀;
+  h.putStrLn xs₀;
+  h.putStrLn xs₂;
+  h.putStrLn xs₁;
+  pure () };
+ys ← withFile fn2 Mode.read $ fun h => h.getLine;
+check_eq "1" (xs₀ ++ xs₀ ++ "\n") ys;
+withFile fn2 Mode.append $ fun h => do
+{ h.putStrLn xs₁;
+  pure () };
+ys ← withFile fn2 Mode.read $ fun h => do
+  { ys ← (List.iota 5).mapM $ fun i => do
+    { ln ← h.getLine;
+      -- IO.println ∘ repr $ ln;
+      b  ← h.isEof;
+      unless (i == 1 || !b) (throw $ IO.userError "isEof");
+      pure ln };
+    b ← h.isEof;
+    unless b (throw $ IO.userError "not isEof");
+    pure ys };
+let rs := [xs₀ ++ xs₀ ++ "\n", xs₂ ++ "\n", xs₁ ++ "\n", xs₁ ++ "\n", ""];
+check_eq "2" rs ys;
+ys ← readFile fn2;
+check_eq "3" (String.join rs) ys;
+pure ()
+
+#eval test2
diff --git a/tests/lean/run/expr1.lean b/tests/lean/run/expr1.lean
index 1c06fac982..dc22007508 100644
--- a/tests/lean/run/expr1.lean
+++ b/tests/lean/run/expr1.lean
@@ -10,7 +10,7 @@ do let f   := mkConst `f [];
    let as₂ := t.getAppRevArgs;
    IO.println as₁;
    IO.println as₂;
-   unless (as₁.reverse == as₂) $ throw "failed";
+   unless (as₁.reverse == as₂) $ throw $ IO.userError "failed";
    pure ()
 
 #eval tst1
@@ -20,7 +20,7 @@ do let l1 := mkLevelMax (mkLevelParam `a) (mkLevelParam `b);
    let l2 := mkLevelMax (mkLevelParam `b) (mkLevelParam `a);
    IO.println l1;
    IO.println l2;
-   unless (Level.isEquiv l1 l2) $ throw "not equiv";
+   unless (Level.isEquiv l1 l2) $ throw $ IO.userError "not equiv";
    pure ()
 
 #eval tst2
@@ -49,12 +49,12 @@ do let f   := mkConst `f [];
    let t2   := mkAppN f #[a, x0];
    let t3   := mkLambda `x BinderInfo.default (mkSort levelZero) (mkAppN f #[a, x0]);
    let t4   := mkLambda `x BinderInfo.default (mkSort levelZero) (mkAppN f #[a, x1]);
-   unless (!t1.hasLooseBVar 0) $ throw "failed-1";
-   unless (t2.hasLooseBVar 0) $ throw "failed-2";
-   unless (!t3.hasLooseBVar 0) $ throw "failed-3";
-   unless (t4.hasLooseBVar 0) $ throw "failed-4";
-   unless (!t4.hasLooseBVar 1) $ throw "failed-5";
-   unless (!t2.hasLooseBVar 1) $ throw "failed-6";
+   unless (!t1.hasLooseBVar 0) $ throw $ IO.userError "failed-1";
+   unless (t2.hasLooseBVar 0) $ throw $ IO.userError "failed-2";
+   unless (!t3.hasLooseBVar 0) $ throw $ IO.userError "failed-3";
+   unless (t4.hasLooseBVar 0) $ throw $ IO.userError "failed-4";
+   unless (!t4.hasLooseBVar 1) $ throw $ IO.userError "failed-5";
+   unless (!t2.hasLooseBVar 1) $ throw $ IO.userError "failed-6";
    pure ()
 
 #eval tst4
@@ -68,27 +68,27 @@ do let f   := mkConst `f [];
    let x2  := mkBVar 2;
    let t   := mkLambda `x BinderInfo.default nat (mkApp f x0);
    IO.println t.etaExpanded?;
-   unless (t.etaExpanded? == some f) $ throw "failed-1";
+   unless (t.etaExpanded? == some f) $ throw $ IO.userError "failed-1";
    let t   := mkLambda `x BinderInfo.default nat (mkApp f x1);
-   unless (t.etaExpanded? == none) $ throw "failed-2";
+   unless (t.etaExpanded? == none) $ throw $ IO.userError "failed-2";
    let t   := mkLambda `x BinderInfo.default nat (mkAppN f #[a, x0]);
-   unless (t.etaExpanded? == some (mkApp f a)) $ throw "failed-3";
+   unless (t.etaExpanded? == some (mkApp f a)) $ throw $ IO.userError "failed-3";
    let t   := mkLambda `x BinderInfo.default nat (mkAppN f #[x0, x0]);
-   unless (t.etaExpanded? == none) $ throw "failed-4";
+   unless (t.etaExpanded? == none) $ throw $ IO.userError "failed-4";
    let t   := mkLambda `x BinderInfo.default nat (mkLambda `y BinderInfo.default nat (mkApp f x0));
-   unless (t.etaExpanded? == none) $ throw "failed-5";
+   unless (t.etaExpanded? == none) $ throw $ IO.userError "failed-5";
    let t   := mkLambda `x BinderInfo.default nat (mkLambda `y BinderInfo.default nat (mkAppN f #[x1, x0]));
    IO.println t;
-   unless (t.etaExpanded? == some f) $ throw "failed-6";
+   unless (t.etaExpanded? == some f) $ throw $ IO.userError "failed-6";
    let t   := mkLambda `x BinderInfo.default nat (mkLambda `y BinderInfo.default nat (mkLambda `z BinderInfo.default nat (mkAppN f #[x2, x1, x0])));
    IO.println t;
-   unless (t.etaExpanded? == some f) $ throw "failed-7";
+   unless (t.etaExpanded? == some f) $ throw $ IO.userError "failed-7";
    let t   := mkLambda `x BinderInfo.default nat (mkLambda `y BinderInfo.default nat (mkLambda `z BinderInfo.default nat (mkAppN f #[a, x2, x1, x0])));
    IO.println t;
-   unless (t.etaExpanded? == some (mkApp f a)) $ throw "failed-8";
+   unless (t.etaExpanded? == some (mkApp f a)) $ throw $ IO.userError "failed-8";
    IO.println t.etaExpanded?;
    let t   := mkApp f a;
-   unless (t.etaExpanded? == some (mkApp f a)) $ throw "failed-9";
+   unless (t.etaExpanded? == some (mkApp f a)) $ throw $ IO.userError "failed-9";
    pure ()
 
 #eval tst5
@@ -102,7 +102,7 @@ IO.println (t1.liftLooseBVars 0 1);
 IO.println (t2.liftLooseBVars 0 1);
 let t3 := (t2.liftLooseBVars 0 1).lowerLooseBVars 1 1;
 IO.println $ t3;
-unless (t2 == t3) $ throw "failed-1";
+unless (t2 == t3) $ throw $ IO.userError "failed-1";
 pure ()
 
 #eval tst6
diff --git a/tests/lean/run/expr_maps.lean b/tests/lean/run/expr_maps.lean
index d098bc0dd2..3487308fe2 100644
--- a/tests/lean/run/expr_maps.lean
+++ b/tests/lean/run/expr_maps.lean
@@ -18,7 +18,7 @@ def exprT3          := mkLambda `x biDef exprNat (mkApp (mkConst `f []) (mkBVar
 def exprT4          := mkLambda `x BinderInfo.implicit exprNat (mkApp (mkConst `f []) (mkBVar 0))
 
 def check (b : Bool) : IO Unit :=
-unless b (throw "failed")
+unless b (throw $ IO.userError "failed")
 
 def tst1 : IO Unit :=
 do IO.println TypeArrowType;
diff --git a/tests/lean/run/print_error.lean b/tests/lean/run/print_error.lean
new file mode 100644
index 0000000000..09c8071d9e
--- /dev/null
+++ b/tests/lean/run/print_error.lean
@@ -0,0 +1,5 @@
+prelude
+import Init.System.IO
+
+def main : IO Unit :=
+throw $ IO.Error.noFileOrDirectory "file.ext" "this is some context"
diff --git a/tests/lean/run/print_error.lean.expected.out b/tests/lean/run/print_error.lean.expected.out
new file mode 100644
index 0000000000..c68d9aeef3
--- /dev/null
+++ b/tests/lean/run/print_error.lean.expected.out
@@ -0,0 +1,2 @@
+uncaught exception: No such file or directory
+  file: file.ext
diff --git a/tests/plugin/Default.lean b/tests/plugin/Default.lean
index b4d574ce82..3dfe24a628 100644
--- a/tests/plugin/Default.lean
+++ b/tests/plugin/Default.lean
@@ -7,7 +7,7 @@ def oh_no : Nat := 0
 def snakeLinter : Linter :=
 fun env n =>
   -- TODO(Sebastian): return actual message with position from syntax tree
-  if n.toString.contains '_' then throw "SNAKES!!"
+  if n.toString.contains '_' then throw $ IO.userError "SNAKES!!"
   else pure MessageLog.empty
 
 @[init]