diff --git a/TODO.md b/TODO.md
index b746ac8..e88b436 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,7 +1,5 @@
 # docs
 
-[docs/lang0] simple README.md like inet
-
 [docs/lang1] update NOTE.md
 [docs/lang1] fix freshen -- be like lang0 with `usedNames`
 
diff --git a/docs/diary/2024-03-29-interpreter-vs-virtual-machine.md b/docs/diary/2024-03-29-interpreter-vs-virtual-machine.md
new file mode 100644
index 0000000..21cb426
--- /dev/null
+++ b/docs/diary/2024-03-29-interpreter-vs-virtual-machine.md
@@ -0,0 +1,8 @@
+---
+title: Interpreter v.s. Virtual Machine
+date: 2024-03-29
+---
+
+Note that, when implementing lambda calculus as an interpreter,
+the depth of the call stack is limited by the hosting language.
+To avoid this limitation we should implement lambda calculus by machine like SECD.
diff --git a/docs/lang0/README.md b/docs/lang0/README.md
index ea9f0e2..72d476a 100644
--- a/docs/lang0/README.md
+++ b/docs/lang0/README.md
@@ -1,28 +1,30 @@
 # Lang0
 
-# Features
+Features:
 
 - Implement call-by-need lazy evaluation.
+- A name must be defined before used, thus no mutual recursion.
+- Allow recursive in top-level definitions by `(fixpoint)`.
 
-- Allow recursive in top-level definitions.
-
-  - No mutual recursion, a name must be defined before used.
-
-- A simple module system with only one API -- `(import)`.
+```scheme
+;; Statement keywords:
 
-  - It can import module from local file or remote URL.
+(define name body)
+(define (name arg ...) body)
+(import "./file.scm")
+(assert-equal exp ...)
+(assert-not-equal exp ...)
 
-- Two simple testing statements `(assert-equal)` and `(assert-not-equal)`.
 
-  - They can handle beta and eta equivalence.
+;; Expression keywords:
 
-Note that, when implementing lambda calculus as an interpreter,
-the depth of the call stack is limited by the hosting language.
-To avoid this limitation we should implement lambda calculus by machine like SECD.
+(lambda (name) ret)
+(fixpoint name body)
+```
 
-# Examples
+## Examples
 
-## Boolean
+### Boolean
 
 ```scheme
 (define (true t f) t)
@@ -38,7 +40,7 @@ To avoid this limitation we should implement lambda calculus by machine like SEC
 (not (not (or true false)))
 ```
 
-## Natural Number by Church encoding
+### Natural Number by Church encoding
 
 [ [WIKIPEDIA](https://en.wikipedia.org/wiki/Church_encoding) ]
 
@@ -56,7 +58,7 @@ To avoid this limitation we should implement lambda calculus by machine like SEC
 (add two two)
 ```
 
-## Factorial
+### Factorial
 
 ```scheme
 (import "./nat-church.scm"
@@ -77,7 +79,7 @@ To avoid this limitation we should implement lambda calculus by machine like SEC
 (factorial three)
 ```
 
-## Factorial by fixpoint combinator
+### Factorial by fixpoint combinator
 
 [ [WIKIPEDIA](https://en.wikipedia.org/wiki/Fixed-point_combinator) ]
 
@@ -117,7 +119,7 @@ To avoid this limitation we should implement lambda calculus by machine like SEC
 (factorial four)
 ```
 
-## Cons the Magnificent
+### Cons the Magnificent
 
 ```scheme
 ;; NOTE Temporarily save `car` and `cdr` to a lambda,
diff --git a/docs/lang1/README.md b/docs/lang1/README.md
index 5ddd149..307b544 100644
--- a/docs/lang1/README.md
+++ b/docs/lang1/README.md
@@ -1,17 +1,13 @@
 # Lang1
 
-## Statements
+```scheme
+;; Statement keywords:
 
-```
-define -- (define name body)
-          (define (name arg ...) body)
-```
+(define name body)
+(define (name arg ...) body)
 
-## Expressions
+;; Expression keywords:
 
-```
-var -- name
-ap  -- (target arg ...)
-fn  -- (lambda (name) ret)
-let -- (let ((name exp) ...) body)
+(lambda (name) ret)
+(let ((name exp) ...) body)
 ```