diff --git a/README.md b/README.md
index db2d4c3..e0259a3 100644
--- a/README.md
+++ b/README.md
@@ -1,3 +1,138 @@
 # NAC3 Specification
 
+Specification and discussions about language design.
+
+## Referencing Python Variables
+> Not decided yet, whether require function annotation or only allow reference
+> to variables.
+
+The kernel is allowed to read Python variables.
+
+Unbounded identifiers would be considered as Python variables, no object is
+allowed. The value would be evaluated at compile time, subsequent modification
+in the host would not be known by the kernel. Basically, only allow lookup, no
+evaluation.
+
+(Bad) Alternative: Evaluate the unbounded identifier, allowing functions and
+objects.  It would easier to write the program as we don't have to manually
+remove function calls in the kernel and store the result in a global variable.
+However, this would potentially cause confusion, as the possibly side-effectful
+function would be evaluated only once during compilation.
+
+(Better) Alternative: only evaluate functions marked as pure? Not sure if we can
+access custom function annotation. We have to rely on the user to uphold the
+guarantee.
+
+Example for a potentially confusing case:
+```py
+from artiq.experiment import *
+counter = 0
+def get_id():
+    counter += 1
+    return counter
+
+class Foo(EnvExperiment):
+    @kernel
+    def run(self):
+        param = get_id()
+        # do something...
+        result = param
+        return result
+```
+
+Example for a totally valid case:
+
+```py
+from artiq.experiment import *
+def get_param(x):
+    return x**2
+
+class Foo(EnvExperiment):
+    @kernel
+    def run(self):
+        # unbounded function call disallowed
+        param = get_param(123)
+        # do something...
+        result = param
+        return result
+```
+
+This would not be allowed, and must be translated into this
+
+```py
+from artiq.experiment import *
+def get_param(x):
+    return x**2
+
+param_123 = get_param(123)
+class Foo(EnvExperiment):
+    @kernel
+    def run(self):
+        param = param_123
+        # do something...
+        result = param
+        return result
+```
+
+## Type
+### Decided
+* Parametric polymorphism: use Python type variable.
+* Normal functions: require full type signature.
+* RPC: optional parameter type signature, require return type signature.
+* No implicit coercion
+
+### Undecided
+#### Class Fields
+Should we require the user to declare all class fields first?
+
+Example:
+```py
+class Foo:
+    a: int32
+    b: int32
+    def __init__(self, a: int32, b: int32):
+        self.a = a
+        self.b = b
+```
+
+#### Subtyping
+Do we allow subtyping? Or is parametric polymorphism enough?
+If subtyping is allowed, we might need virtual method table.
+
+Example where parametric polymorphism is not enough:
+```py
+class Base:
+    def foo();
+        return 1
+
+class Foo(Base):
+    def foo();
+        return 2
+
+def run_all(l: list[Base]):
+    return [x.foo() for x in l]
+
+run_all([Base(), Foo()])
+```
+
+#### Union Type
+As function overloading is not possible, should we allow union type, and const
+evaluate all the type checks after monomorphization?
+
+Example:
+```py
+def foo(x: Union[int, bool]):
+    if type(x) == int:
+        return x
+    else:
+        return 1 if x else 0
+```
+
+## Function Pointers
+- Lambda with no capturing are treated as normal functions.
+- Lambda with capturing: a structure would be created to store *pointers* to
+  captured variables, and the lambda would be a method of the struct.
+  (Note: Storing pointers to meet the binding behavior of Python lambda)
+- Method: implemented with fat pointer, i.e. function pointer + object pointer.
+  Subject to lifetime rules.