feat(summary): write executive summary

summary/exec_summary.typ

@@ -10,21 +10,118 @@
 
 #import "@preview/isc-hei-exec-summary:0.8.1" : *
 #import "../meta.typ"
+#import "../report/figs/architecture.typ"
+#import "@local/codly:1.3.1": codly, codly-init, local
+#import "@preview/codly-languages:0.1.10": codly-languages
 
 // Must be <= 365 characters long.
-#let summary = "Midas is cool!" // TODO
+#let summary = "Midas is a type system built on top of Python to provide both static type checking and runtime assertions. It includes its own type definition language, implements dependent types in the form of constraint expressions and offers extended checking of dataframe schemas and operations."
 
 #assert(
   summary.len() <= 365,
   message: "Summary too long: len() > 365"
 )
 
-#let content = [
-  #todo[]
+#show: codly-init
+#codly(
+  languages: codly-languages
+    + (
+      midas: (
+        name: "Midas",
+        color: rgb("#eedd47"),
+        icon: box(
+          image(
+            "../assets/icon.svg",
+            height: 130%,
+            fit: "contain",
+          ),
+        ),
+      ),
+    ),
+)
 
-  #lorem-pars(500)
-  #colbreak()
-  #lorem-pars(500)
+#set raw(
+  syntaxes: path("../midas.sublime-syntax")
+)
+#show raw.where(block: true): set text(size: 0.9em)
+
+#let content = [
+  = Objectives
+
+  Python is a very popular language known for its great flexibility. For beginners and many developers, its duck-typing philosophy is a great way to code quickly and without heavy syntax. However, it is extremely easy to mix things up, use the wrong variable or not realize that a value has the wrong type.
+  
+  Additionally, in data science, most of the values handled by a program are only known at runtime, because they are loaded from a dataset or fetched from an external service.
+
+  Enter Midas, a new type system designed to allow developers to define custom types for their use case, check their script to avoid type errors and generate safe runtime code that will ensure data integrity. For data engineers, Midas also allows defining value constraints and will verify operations on Pandas DataFrames.
+
+  #codly(
+    header: [types.midas]
+  )
+  #figure(
+    ```midas
+    predicate not_empty(text: str) = len(text) != 0
+    type Height = float where _ >= 0
+    alias People = Frame[
+        name: str where not_empty(_),
+        height: Height
+    ]
+    ```,
+    caption: [Example custom type definitions]
+  )
+
+  = Explanation
+
+  Midas was developed in a modular fashion, adding features one-by-one, starting with the selection of a subset of the Python language to support and the design of a definition language. Then a parser was built to read in Midas files. After defining some formal typing rules, the first elements of the type checker were put in place to handle basic Python statements and expressions.
+
+  The type system was then extended to support subtyping, generics, methods and more. After implementing cast expressions, the code generator was developed and integrated in the compilation pipeline.
+  
+  Once a strong foundation was laid out it was further strengthened with numerous other features, such as constraint types and type checking of dataframe operations. The latter allows powerful inference of some aggregation result types.
+
+  #codly(
+    header: [script.py],
+    highlights: (
+      (
+        line: 3,
+        start: 11,
+        tag: [#h(2pt)Column[Height]],
+        fill: blue.lighten(60%)
+      ),
+      (
+        line: 4,
+        start: 17,
+        tag: [#h(2pt)Height],
+        fill: blue.lighten(60%)
+      ),
+    )
+  )
+  #figure(
+    ```python
+    import pandas as pd
+    people: People = cast(People, pd.read_csv(...))
+    heights = people["height"]
+    median_height = heights.median()
+    ```,
+    caption: [Example type checking of dataframe operations]
+  )
+
+  = Conclusion
+
+  This project provides a solid hybrid type system for Python, that helps data engineers and developers avoid costly mistakes. It is packed with many useful features such as runtime checking of cast expressions and constraint types. Its modular architecture makes it easily expandable too.
+
+  Some ideas for future extensions include adding a constraint solver, handling reference types and supporting multi-file projects through import statements.
+
+  #place(
+    bottom + center,
+    scope: "parent",
+    float: true,
+    figure(
+      {
+        set par(justify: false)
+        architecture.overview
+      },
+      caption: [Implementation architecture overview]
+    )
+  )
 ]
 
 #show: exec-summary.with(