Collapse Theory/Runtime sections

docs/source/articles/What-Are-Proofs.md

@@ -22,7 +22,7 @@ main : Spec
   negate
 ```
 
-But if you change any of the returned bools, it won't work anymore. It is literally impossible to make anything other than a boolean negation pass! This extreme expressiveness of the type language allows you to specify complex properties about software. For example, this one:
+But if you change any of the returned bools, it won't work anymore. It is literally impossible to make anything other than a boolean negation pass! In other words, a term of type `Spec` **proves** he specification represented by it. That's what theorem proving is; it is nothing but a fancy way to say *"type-checking in a language that has very precise types"*. And Formality types can be arbitrarily expressive. For example, this `Spec`:
 
 ```javascript
 Spec : Type
@@ -33,7 +33,7 @@ Spec : Type
     } -> [x : A ~ At(A,x,len,idx,vec)] // Returns the element `x` that is at index `idx` of that `vec`
 ```
 
-specifies an array accessor that can't have an out-of-bounds error, and that can't return the wrong element! If OpenSSL proved that Spec, we wouldn't have Heartbleed. And the cool thing is that those proofs happen statically, they have zero runtime costs!
+specifies an array accessor that can't have an out-of-bounds error, and that can't return the wrong element! If OpenSSL proved it, we wouldn't have Heartbleed. And the cool thing is that those proofs happen statically, they have zero runtime costs!
 
 In the context of smart-contracts, we could have specs like "this contract's balance satisfies certain invariant", completely preventing things like TheDAO being drained. Of course, proofs can be huge and ugly, but that's ok, developers are paid to work hard and write good software. The point is to have a small list of simple specifications that users can read and be confident the smart-contract behaves as desired, without having to trust its developers.
 

docs/source/index.rst

@@ -34,19 +34,13 @@ Table of contents
    language/4.Core-Features
    language/5.Datatypes
 
-.. toctree::
-    :maxdepth: 2
-    :numbered:
-    :caption: Runtime
-
-    runtime/Formality-Net
-
 .. toctree::
     :maxdepth: 2
     :numbered:
     :caption: Theory
 
-    theory/TODO
+    theory/Formality-Net
+    theory/Self-Types
 
 .. toctree::
     :maxdepth: 2
@@ -64,4 +58,4 @@ Table of contents
     :caption: Articles
     :numbered:
 
-    tutorials/What-Are-Proofs
+    articles/What-Are-Proofs

docs/source/language/1.Motivation.md

@@ -18,6 +18,6 @@ Formality's substitution algorithm is **asymptotically faster** than Haskell's,
 
 Formality's unique approach to termination is conjectured to allow it to have elegant, powerful type-level features that would be otherwise impossible without causing logical inconsistencies. For example, instead of built-in datatypes, we rely on [Self Types](https://www.semanticscholar.org/paper/Self-Types-for-Dependently-Typed-Lambda-Encodings-Fu-Stump/652f673e13b889e0fd7adbd480c2fdf290621f66), which allow us to implement inductive families with native lambdas. As history tells, having elegant foundations often pays back. We've not only managed to port several proofs from other assistants, but found techniques to [emulate Coq's structural recursion](https://github.com/moonad/Formality-Base/commit/b777d806c6fa37f2ce306fbe87b3ed267152b90c), to perform large eliminations, and even an hypothetical encoding of [higher inductive types](https://github.com/moonad/Formality-Base/blob/master/Example.HigherInductiveType.fm); and we've barely began exploring the system.
 
-![](https://github.com/moonad/formality/raw/master/docs/images/inet-simulation.gif)
+![](https://github.com/moonad/formality/raw/master/archive/images/inet-simulation.gif)
 
 *Interaction Net (inet) simulation*

docs/source/runtime/Formality-Net.md → docs/source/theory/Formality-Net.md

@@ -6,7 +6,7 @@ main one, plus a list of "rewrite rules" that are activated whenever two nodes
 are connected by their main ports. Our system includes 6 types of nodes, ERA,
 CON, OP1, OP2, ITE, NUM.
 
-![](https://raw.githubusercontent.com/moonad/Formality/master/docs/images/fm-net-node-types.png)
+![](https://raw.githubusercontent.com/moonad/Formality/master/archive/images/fm-net-node-types.png)
 
 - `CON` has 3 ports and an integer label. It is used to represent lambdas,
   applications, boxes (implicitly) and duplications. Since FM-Core is based on
@@ -37,7 +37,7 @@ In order to perform computations, FM-Net has a set of rewrite rules that are
 triggered whenever two nodes are connected by their main ports. This is an
 extensive list of those rules:
 
-![](https://raw.githubusercontent.com/moonad/Formality/master/docs/images/fm-net-rewrite-rules.png)
+![](https://raw.githubusercontent.com/moonad/Formality/master/archive/images/fm-net-rewrite-rules.png)
 
 Note that, while there are many rules (since we need to know what to do on each
 combination of a node), most of those have the same "shape" (such as OP2-OP2,
@@ -98,7 +98,7 @@ Those rules allow us to add, multiply, divide and so on native numbers.
 The process of compiling FM-Core to FM-Net can be defined by the following
 function `k_b(net)`:
 
-![](https://raw.githubusercontent.com/moonad/Formality/master/docs/images/fm-net-compilation.png)
+![](https://raw.githubusercontent.com/moonad/Formality/master/archive/images/fm-net-compilation.png)
 
 This function recursively walks through a term, creating nodes and "temporary
 variables" (`x_b`) in the process. It also keeps track of the number of boxes it

docs/source/theory/Self-Types.md

@@ -0,0 +1,3 @@
+# Self-Types
+
+(TODO)