diff --git a/_01.Language-basics.sz b/_01.Language-basics.sz
index 3cad378..1844606 100644
--- a/_01.Language-basics.sz
+++ b/_01.Language-basics.sz
@@ -24,21 +24,20 @@ git pull
 
 @subsection{Your first bjolang program}
 
-Bjolang compiles to c#. Many of the design decisions behind bjolang stems from this limitation. The first one you will encounter is that a program needs a main function. like the one in c#, that returns an int. If execution ended correctly it should return 0 if the program executed successfully. 
+Bjolang compiles to c#. Many of the design decisions behind bjolang stems from this limitation. The first one you will encounter is that a program needs a main function, like the one in c#. An int it returns is the program's exit code, 0 when it ran correctly; a main that returns anything else exits with 0.
 
 @codeblock[#:lang "bjolang"]{
-(: print-hello (-> string unit))
+(: print-hello (-> string void))
 (defun (print-hello name)
   (println (str "Hello, " name "!")))
 
 (defun (main args)
-  (print-hello "User")
-  0)
+  (print-hello "User"))
 }
 
 This can then be run using @code{bjo run filename}, and it should print @code{Hello, User!}. 
 
-What you can see here is that defun is the form for defining a function. main is special, it needs no type declaration. print-hello is a regular function, and thus has to declare its type. Everything at toplevel needs to do that. The form is (: name type). A function type is declared as (-> ArgType ... Return-Type). print-hello takes a string argument and returns unit. unit is the name for nothing.
+What you can see here is that defun is the form for defining a function. main is special, it needs no type declaration. print-hello is a regular function, and thus has to declare its type. Everything at toplevel needs to do that. The form is (: name type). A function type is declared as (-> ArgType ... Return-Type). print-hello takes a string argument and returns void. void is the name for nothing: the unit type, whose one value is what println gives back.
 
 @subsection{Declaring types}
 For most of your bjolang code, you will only declare types in the top level. Types within functions are inferred, so declaring types there is almost never necessary. A value type is declared just like a function, but without the function type declaration:
@@ -62,7 +61,7 @@ You can also declare your own types. Either aliases of other types, records of y
 This can then be destructed using pattern matching.
 
 @codeblock[#:lang "bjolang"]{
-(: print-user (-> User unit))
+(: print-user (-> User void))
 (defun (print-user u)
   (match u
     ;; Subpatterns: here we match name, age, the Card rank
@@ -119,14 +118,14 @@ A function takes any number of arguments and produces a value. The signature of
   ;; the last expression in the body is the return value
   (* x 2))
 
-(:print-n-times (-> string int unit))
+(: print-n-times (-> string int void))
 (defun (print-n-times what n)
   (loop (:for i (up-from 0 #:to n))
-    (println what)))
+    (:do (println what))))
 
 ;; call twice takes a function take takes an argument
-;; of type %a and returns unit. 
-(: call-twice (-> (-> %a unit) %a unit))
+;; of type %a and returns void.
+(: call-twice (-> (-> %a void) %a void))
 (defun (call-twice f val)
   (f val)
   (f val))
diff --git a/_04.Appendices.sz b/_04.Appendices.sz
index 5a2cd06..26c6767 100644
--- a/_04.Appendices.sz
+++ b/_04.Appendices.sz
@@ -67,12 +67,12 @@ When compiled, the frontend rejects this with:
 Type Error: Function 'greet' requires a type signature (: greet ...) at hello.bjo:1:1
 }|
 
-@strong{Why it happens:} Unlike local helper functions defined inside another function, every top-level definition in a module must carry an explicit type signature. The compiler requires this so that module interfaces are self-documenting and can be emitted into the compiled assembly's public metadata without requiring whole-program inference across files. The only exception is @code{main}, which has a fixed signature known to the compiler.
+@strong{Why it happens:} Unlike local helper functions defined inside another function, every top-level definition in a module must carry an explicit type signature. The compiler requires this so that module interfaces are self-documenting and can be emitted into the compiled assembly's public metadata without requiring whole-program inference across files. The only exception is @code{main}: the compiler knows what it takes, the arguments as a @code{(Vec string)}, and what it returns is the exit code when it is an int.
 
 @strong{How to fix it:} Add an explicit signature right before the definition:
 
 @codeblock[#:lang "bjolang"]|{
-(: greet (-> string unit))
+(: greet (-> string void))
 (defun (greet name)
   (println (str "Hello, " name)))
 }|