diff --git a/docs/spec/overview.md b/docs/spec/overview.md
index 0fec260e9b6d187ba790b8dcfeaf83dde4d7d07b..41d5658f5c02618c9d8ce6fff657f0ca04b82a0a 100644
--- a/docs/spec/overview.md
+++ b/docs/spec/overview.md
@@ -12,4 +12,5 @@ Please view the following documents (in roughly this order):
 2. definitions.md
 3. statements.md
 4. expressions.md
-5. validation.md
\ No newline at end of file
+5. validation.md
+6. types.md
\ No newline at end of file
diff --git a/docs/spec/types.md b/docs/spec/types.md
new file mode 100644
index 0000000000000000000000000000000000000000..5d2f6361aafa73fb7fc013735229e6338593fcda
--- /dev/null
+++ b/docs/spec/types.md
@@ -0,0 +1,7 @@
+# Types
+
+To write
+
+# Type Inference
+
+To write
\ No newline at end of file
diff --git a/docs/spec/validation.md b/docs/spec/validation.md
index 9a0fa0b9419e50dce43024c892d7c4f5fc0e9525..e577ff176d634b1003a612f7432e4834f1897bb0 100644
--- a/docs/spec/validation.md
+++ b/docs/spec/validation.md
@@ -158,6 +158,10 @@ The `TypeRef` for a function call should resolve to either a builtin function, o
 
 The `TypeRef` for a component call should resolve to either a builtin component, or a user-defined component. Component calls, like function calls, must following the rules for polymorphic arguments and the arguments to the components themselves. Furthermore component "call" expressions may only be placed with a `StmtNew` as parent. That is to say: one doesn't really call components, instead one instantiates them.
 
+### Casting Expressions
+
+Casting expressions take 1 polymorphic argument (the type that the expression is casting to), for which the default polymorphic argument rules apply. This causes a cast without an explicit output type to become an implicit cast. Apart from that its correctness is governed by the type checker.across
+
 ## Builtin Procedures
 
 Several functions are builtin procedures in the language. We'll shortly provide their meaning and their syntax here. Some of these functions cannot be expressed in PDL itself, so some ad-hoc syntax is used instead.
@@ -241,9 +245,24 @@ func assert(bool test) -> void { /* ... */ }
 
 Synchronous blocks may only be placed in primitive components. Synchronous blocks may not be nested. One may not jump into or out of a synchronous block.
 
+### Component Instantiation with New
+
+The "new" statement may only occur within the body of a composite component definition.
+
+**note**: This requirement may be dropped in the future.
+
 ### Use of Builtin Procedures
 
 Builtin procedures that do not have a return value (currently only `put` and `assert`) may not be called at the expression level and must be called at the statement level. i.e. the parent of the builtin call expression may only be the `StmtExpr` statement.
 
+**note**: Perhaps this is all a bit convoluted, and we should simply define them as statements in the grammar itself? Although then this "validation" section becomes more complicated?
+
 ### Control-Flow Rules
 
+There are several control-flow statements in the language. For all of them we have the rule that they may not cause the code to exit a synchronous block. Because no control-flow statement can jump to inner scopes, there can be no possiblity of jumping into a synchronous block.
+
+Naturally the break/continue statements must be nested in the body of a loop statement. If they are specified with a label, then the inner statement of a labeled statement must be a loop statement, and the break/continue statement must be nested within that targeted loop.
+
+The return statement may only appear within function bodies. It must have as many return expressions as the function declaration defines return types. **note**: Although at the moment, there is only ever one return type.
+
+The goto statement may only jump to labels in the same or outer scopes. It may skip to a label inside the current scope, but defined at a later position than the goto statement. The goto statement may not jump over variable declarations (and implicit initialization) inside its target scope.
\ No newline at end of file