Update snowflake thesis outline

outline-snowflake.md

@@ -13,3 +13,46 @@ We build Refinement Types for Rust on top of its Ownership and Borrowing System.
 3. *Climax:* We combine the semantics and proof the consistency of the combined semantics.
 4. *Falling Action:* We implement the formal verification engine Verdigris.
 5. *Catastrophe:* We test Verdigris on itself and on parts of the metrology cloud.
+
+## Elaborate into sections (and subsections)
+
+1. Exposition
+  - What is Rust?
+    - Goals
+    - Basic syntax
+  - What is ownership?
+    - move semantics
+    - `Drop`
+    - copy semantics
+  - What is borrowing?
+    - Shared and unique references
+    - Lifetimes
+    - Non-Lexical lifetimes
+    - Two-phase borrowing and the borrow stack
+    - loans and regions
+  - What are refinement types?
+  - Which other type system enhancements are there?
+    - Relevant types and `#[must_use]`
+    - Linear, uniqueness and ordered types
+    - Totality and termination metrics
+    - Purity and (algebraic) effects
+2. Rising Moment
+  - Patina, Featherweight Rust, KRust, and RustHorn (and Prusti?)
+  - RustSEM, Oxide, and Polonius
+  - Discussion on RustSEM, Oxide, and Polonius
+  - Simple-R, Rondon-RT, and Vekris-RT (and more?)
+  - Discussion on refinement type semantics
+3. Climax
+  - Extracting a semantics from Polonius (?)
+  - The complete semantics
+  - Progress and Preservation (?)
+4. Falling Action
+  - Setup: Used frameworks/libraries
+  - Used techniques
+  - Measurements (test coverage, time effort, …)
+5. Catastrophe
+  - What to measure? Which experiments to conduct?
+  - Verdigris in itself: Findings
+  - Effort: time and code changes
+  - Verdigris for DATAPOLIS
+  - Conclusion
\ No newline at end of file