Update index.

This reverts commit 5cc92d3a9d.

assets/scss/gametheory.scss

@@ -0,0 +1,11 @@
+@import "variables.scss";
+@import "mixins.scss";
+
+.assumption-number {
+    font-weight: bold;
+}
+
+.assumption {
+    @include bordered-block;
+    padding: 0.8rem;
+}

code/aoc-coq/day1.v

@@ -0,0 +1,102 @@
+Require Import Coq.Lists.List.
+Require Import Omega.
+
+Definition has_pair (t : nat) (is : list nat) : Prop :=
+  exists n1 n2 : nat, n1 <> n2 /\ In n1 is /\ In n2 is /\ n1 + n2 = t.
+
+Fixpoint find_matching (is : list nat) (total : nat) (x : nat) : option nat :=
+  match is with
+  | nil => None
+  | cons y ys =>
+      if Nat.eqb (x + y) total
+      then Some y
+      else find_matching ys total x 
+  end.
+
+Fixpoint find_sum (is : list nat) (total : nat) : option (nat * nat) :=
+  match is with
+  | nil => None
+  | cons x xs =>
+      match find_matching xs total x with
+      | None => find_sum xs total (* Was buggy! *)
+      | Some y => Some (x, y)
+      end
+  end.
+
+Lemma find_matching_correct : forall is k x y,
+  find_matching is k x = Some y -> x + y = k.
+Proof.
+  intros is. induction is;
+  intros k x y Hev.
+  - simpl in Hev. inversion Hev.
+  - simpl in Hev. destruct (Nat.eqb (x+a) k) eqn:Heq.
+    + injection Hev as H; subst.
+      apply EqNat.beq_nat_eq. auto.
+    + apply IHis. assumption.
+Qed.
+
+Lemma find_matching_skip : forall k x y i is,
+  find_matching is k x = Some y -> find_matching (cons i is) k x = Some y.
+Proof.
+  intros k x y i is Hsmall.
+  simpl. destruct (Nat.eqb (x+i) k) eqn:Heq.
+  - apply find_matching_correct in Hsmall.
+    symmetry in Heq. apply EqNat.beq_nat_eq in Heq.
+    assert (i = y). { omega. } rewrite H. reflexivity.
+  - assumption.
+Qed.
+
+Lemma find_matching_works : forall is k x y, In y is /\ x + y = k ->
+  find_matching is k x = Some y.
+Proof.
+  intros is. induction is;
+  intros k x y [Hin Heq].
+  - inversion Hin.
+  - inversion Hin.
+    + subst a. simpl. Search Nat.eqb.
+      destruct (Nat.eqb_spec (x+y) k).
+      * reflexivity.
+      * exfalso. apply n. assumption.
+    + apply find_matching_skip. apply IHis.
+      split; assumption.
+Qed.
+
+Theorem find_sum_works :
+  forall k is, has_pair k is ->
+  exists x y, (find_sum is k = Some (x, y) /\ x + y = k).
+Proof.
+  intros k is. generalize dependent k.
+  induction is; intros k [x' [y' [Hneq [Hinx [Hiny Hsum]]]]].
+  - (* is is empty. But x is in is! *)
+    inversion Hinx.
+  - (* is is not empty. *)
+    inversion Hinx. 
+    + (* x is the first element. *)
+      subst a. inversion Hiny.
+      * (* y is also the first element; but this is impossible! *)
+        exfalso. apply Hneq. apply H.
+      * (* y is somewhere in the rest of the list.
+           We've proven that we will find it! *)
+        exists x'. simpl.
+        erewrite find_matching_works.
+        { exists y'. split. reflexivity. assumption. }
+        { split; assumption. }
+    + (* x is not the first element. *)
+      inversion Hiny.
+      * (* y is the first element,
+           so x is somewhere in the rest of the list.
+           Again, we've proven that we can find it. *)
+        subst a. exists y'. simpl.
+        erewrite find_matching_works.
+        { exists x'. split. reflexivity. rewrite plus_comm. assumption. }
+        { split. assumption. rewrite plus_comm. assumption. }
+      * (* y is not the first element, either.
+           Of course, there could be another matching pair
+           starting with a. Otherwise, the inductive hypothesis applies. *)
+        simpl. destruct (find_matching is k a) eqn:Hf.
+        { exists a. exists n. split.
+          reflexivity. 
+          apply find_matching_correct with is. assumption. }
+        { apply IHis. unfold has_pair. exists x'. exists y'.
+          repeat split; assumption. }
+Qed.

code/typesafe-imperative/TypesafeImp.idr

@@ -0,0 +1,102 @@
+data Reg = A | B | R
+
+data Ty = IntTy | BoolTy
+
+TypeState : Type
+TypeState = (Ty, Ty, Ty)
+
+getRegTy : Reg -> TypeState -> Ty
+getRegTy A (a, _, _) = a
+getRegTy B (_, b, _) = b
+getRegTy R (_, _, r) = r
+
+setRegTy : Reg -> Ty -> TypeState -> TypeState
+setRegTy A a (_, b, r) = (a, b, r)
+setRegTy B b (a, _, r) = (a, b, r)
+setRegTy R r (a, b, _) = (a, b, r)
+
+data Expr : TypeState -> Ty -> Type where
+  Lit : Int -> Expr s IntTy
+  Load : (r : Reg) -> Expr s (getRegTy r s)
+  Add : Expr s IntTy -> Expr s IntTy -> Expr s IntTy
+  Leq : Expr s IntTy -> Expr s IntTy -> Expr s BoolTy
+  Not : Expr s BoolTy -> Expr s BoolTy
+
+mutual
+  data Stmt : TypeState -> TypeState -> TypeState -> Type where
+    Store : (r : Reg) -> Expr s t -> Stmt l s (setRegTy r t s)
+    If : Expr s BoolTy -> Prog l s n -> Prog l s n -> Stmt l s n
+    Loop : Prog s s s -> Stmt l s s
+    Break : Stmt s s s
+
+  data Prog : TypeState -> TypeState -> TypeState -> Type where
+    Nil : Prog l s s
+    (::) : Stmt l s n -> Prog l n m -> Prog l s m
+
+initialState : TypeState
+initialState = (IntTy, IntTy, IntTy)
+
+testProg : Prog Main.initialState Main.initialState Main.initialState
+testProg =
+  [ Store A (Lit 1 `Leq` Lit 2)
+  , If (Load A)
+    [ Store A (Lit 1) ]
+    [ Store A (Lit 2) ]
+  , Store B (Lit 2)
+  , Store R (Add (Load A) (Load B))
+  ]
+
+prodProg : Prog Main.initialState Main.initialState Main.initialState
+prodProg =
+  [ Store A (Lit 7)
+  , Store B (Lit 9)
+  , Store R (Lit 0)
+  , Loop
+    [ If (Load A `Leq` Lit 0)
+      [ Break ]
+      [ Store R (Load R `Add` Load B)
+      , Store A (Load A `Add` Lit (-1))
+      ]
+    ]
+  ]
+
+repr : Ty -> Type
+repr IntTy = Int
+repr BoolTy = Bool
+
+data State : TypeState -> Type where
+  MkState : (repr a, repr b, repr c) -> State (a, b, c)
+
+getReg : (r : Reg) -> State s -> repr (getRegTy r s)
+getReg A (MkState (a, _, _)) = a
+getReg B (MkState (_, b, _)) = b
+getReg R (MkState (_, _, r)) = r
+
+setReg : (r : Reg) -> repr t -> State s -> State (setRegTy r t s)
+setReg A a (MkState (_, b, r)) = MkState (a, b, r)
+setReg B b (MkState (a, _, r)) = MkState (a, b, r)
+setReg R r (MkState (a, b, _)) = MkState (a, b, r)
+
+expr : Expr s t -> State s -> repr t
+expr (Lit i) _ = i
+expr (Load r) s = getReg r s
+expr (Add l r) s = expr l s + expr r s
+expr (Leq l r) s = expr l s <= expr r s
+expr (Not e) s = not $ expr e s
+
+mutual
+  stmt : Stmt l s n -> State s -> Either (State l) (State n)
+  stmt (Store r e) s = Right $ setReg r (expr e s) s
+  stmt (If c t e) s = if expr c s then prog t s else prog e s
+  stmt (Loop p) s =
+    case prog p s >>= stmt (Loop p) of
+      Right s => Right s
+      Left s => Right s
+  stmt Break s = Left s
+
+  prog : Prog l s n -> State s -> Either (State l) (State n)
+  prog Nil s = Right s
+  prog (st::p) s = stmt st s >>= prog p
+
+run : Prog l s l -> State s -> State l
+run p s = either id id $ prog p s

config.toml

@@ -6,6 +6,15 @@ pygmentsCodeFences = true
 pygmentsUseClasses = true
 summaryLength = 20
 
+[outputFormats]
+  [outputFormats.Toml]
+    name = "toml"
+    mediaType = "application/toml"
+    isHTML = false
+
+[outputs]
+  home = ["html","rss","toml"]
+
 [markup]
   [markup.tableOfContents]
     endLevel = 4

content/blog/00_aoc_coq.md

@@ -0,0 +1,350 @@
+---
+title: "Advent of Code in Coq - Day 1"
+date: 2020-12-02T18:44:56-08:00
+tags: ["Advent of Code", "Coq"]
+---
+
+The first puzzle of this year's [Advent of Code](https://adventofcode.com) was quite
+simple, which gave me a thought: "Hey, this feels within reach for me to formally verify!"
+At first, I wanted to formalize and prove the correctness of the [two-pointer solution](https://www.geeksforgeeks.org/two-pointers-technique/).
+However, I didn't have the time to mess around with the various properties of sorted
+lists and their traversals. So, I settled for the brute force solution. Despite
+the simplicity of its implementation, there is plenty to talk about when proving
+its correctness using Coq. Let's get right into it!
+
+Before we start, in the interest of keeping the post self-contained, here's the (paraphrased)
+problem statement:
+
+> Given an unsorted list of numbers, find two distinct numbers that add up to 2020.
+
+With this in mind, we can move on to writing some Coq!
+
+### Defining the Functions
+The first step to proving our code correct is to actually write the code! To start with,
+let's write a helper function that, given a number `x`, tries to find another number
+`y` such that `x + y = 2020`. In fact, rather than hardcoding the desired
+sum to `2020`, let's just use another argument called `total`. The code is quite simple:
+
+{{< codelines "Coq" "aoc-coq/day1.v" 7 14 >}}
+
+Here, `is` is the list of numbers that we want to search.
+We proceed by case analysis: if the list is empty, we can't
+find a match, so we return `None` (the Coq equivalent of Haskell's `Nothing`).
+On the other hand, if the list has at least one element `y`, we see if it adds
+up to `total`, and return `Some y` (equivalent to `Just y` in Haskell) if it does.
+If it doesn't, we continue our search into the rest of the list.
+
+It's somewhat unusual, in my experience, to put the list argument first when writing
+functions in a language with [currying](https://wiki.haskell.org/Currying). However,
+it seems as though Coq's `simpl` tactic, which we will use later, works better
+for our purposes when the argument being case analyzed is given first.
+
+We can now use `find_matching` to define our `find_sum` function, which solves part 1.
+Here's the code:
+
+{{< codelines "Coq" "aoc-coq/day1.v" 16 24 >}}
+
+For every `x` that we encounter in our input list `is`, we want to check if there's
+a matching number in the rest of the list. We only search the remainder of the list
+because we can't use `x` twice: the `x` and `y` we return that add up to `total`
+must be different elements. We use `find_matching` to try find a complementary number
+for `x`. If we don't find it, this `x` isn't it, so we recursively move on to `xs`.
+On the other hand, if we _do_ find a matching `y`, we're done! We return `(x,y)`,
+wrapped in `Some` to indicate that we found something useful.
+
+What about that `(* Was buggy! *)` line? Well, it so happens that my initial
+implementation had a bug on this line, one that came up as I was proving
+the correctness of my function. When I wasn't able to prove a particular
+behavior in one of the cases, I realized something was wrong. In short,
+my proof actually helped me find and fix a bug!
+
+This is all the code we'll need to get our solution. Next, let's talk about some
+properties of our two functions.
+
+### Our First Lemma
+When we call `find_matching`, we want to be sure that if we get a number, 
+it does indeed add up to our expected total. We can state it a little bit more
+formally as follows:
+
+> For any numbers `k` and `x`, and for any list of number `is`,
+> if `find_matching is k x` returns a number `y`, then `x + y = k`.
+
+And this is how we write it in Coq:
+
+{{< codelines "Coq" "aoc-coq/day1.v" 26 27 >}}
+
+The arrow, `->`, reads "implies". Other than that, I think this
+property reads pretty well. The proof, unfortunately, is a little bit more involved.
+Here are the first few lines:
+
+{{< codelines "Coq" "aoc-coq/day1.v" 28 31 >}}
+
+We start with the `intros is` tactic, which is akin to saying
+"consider a particular list of integers `is`". We do this without losing
+generality: by simply examining a concrete list, we've said nothing about
+what that list is like. We then proceed by induction on `is`.
+
+To prove something by induction for a list, we need to prove two things:
+
+* The __base case__. Whatever property we want to hold, it must
+hold for the empty list, which is the simplest possible list.
+In our case, this means `find_matching` searching an empty list.
+* The __inductive case__. Assuming that a property holds for any list
+`[b, c, ...]`, we want to show that the property also holds for 
+the list `[a, b, c, ...]`. That is, the property must remain true if we
+prepend an element to a list for which this property holds.
+
+These two things combined give us a proof for _all_ lists, which is exactly
+what we want! If you don't belive me, here's how it works. Suppose you want
+to prove that some property `P` holds for `[1,2,3,4]`. Given the base
+case, we know that `P []` holds. Next, by the inductive case, since
+`P []` holds, we can prepend `4` to the list, and the property will
+still hold. Thus, `P [4]`. Now that `P [4]` holds, we can again prepend
+an element to the list, this time a `3`, and conclude that `P [3,4]`.
+Repeating this twice more, we arrive at our desired fact: `P [1,2,3,4]`.
+
+When we write `induction is`, Coq will generate two proof goals for us,
+one for the base case, and one for the inductive case. We will have to prove
+each of them separately. Since we have
+not yet introduced the variables `k`, `x`, and `y`, they remain
+inside a `forall` quantifier at that time. To be able to refer
+to them, we want to use `intros`. We want to do this in both the
+base and the inductive case. To quickly do this, we use Coq's `;`
+operator. When we write `a; b`, Coq runs the tactic `a`, and then
+runs the tactic `b` in every proof goal generated by `a`. This is
+exactly what we want.
+
+There's one more variable inside our second `intros`: `Hev`.
+This variable refers to the hypothesis of our statement:
+that is, the part on the left of the `->`. To prove that `A`
+implies `B`, we assume that `A` holds, and try to argue `B` from there.
+Here is no different: when we use `intros Hev`, we say, "suppose that you have
+a proof that `find_matching` evaluates to `Some y`, called `Hev`". The thing
+on the right of `->` becomes our proof goal.
+
+Now, it's time to look at the cases. To focus on one case at a time,
+we use `-`. The first case is our base case. Here's what Coq prints
+out at this time:
+
+```
+k, x, y : nat
+Hev : find_matching nil k x = Some y
+
+========================= (1 / 1)
+
+x + y = k
+```
+
+All the stuff above the `===` line are our hypotheses. We know
+that we have some `k`, `x`, and `y`, all of which are numbers.
+We also have the assumption that `find_matching` returns `Some y`.
+In the base case, `is` is just `[]`, and this is reflected in the
+type for `Hev`. To make this more clear, we'll simplify the call to `find_matching`
+in `Hev`, using `simpl in Hev`. Now, here's what Coq has to say about `Hev`:
+
+```
+Hev : None = Some y
+```
+
+Well, this doesn't make any sense. How can something be equal to nothing?
+We ask Coq this question using `inversion Hev`. Effectively, the question
+that `inversion` asks is: what are the possible ways we could have acquired `Hev`?
+Coq generates a proof goal for each of these possible ways. Alas, there are
+no ways to arrive at this contradictory assumption: the number of proof sub-goals
+is zero. This means we're done with the base case!
+
+The inductive case is the meat of this proof. Here's the corresponding part
+of the Coq source file:
+
+{{< codelines "Coq" "aoc-coq/day1.v" 32 36 >}}
+
+This time, the proof state is more complicated:
+
+```
+a : nat
+is : list nat
+IHis : forall k x y : nat, find_matching is k x = Some y -> x + y = k
+k, x, y : nat
+Hev : find_matching (a :: is) k x = Some y
+
+========================= (1 / 1)
+
+x + y = k
+```
+
+Following the footsteps of our informal description of the inductive case,
+Coq has us prove our property for `(a :: is)`, or the list `is` to which
+`a` is being prepended. Like before, we assume that our property holds for `is`.
+This is represented in the __induction hypothesis__ `IHis`. It states that if
+`find_matching` finds a `y` in `is`, it must add up to `k`. However, `IHis`
+doesn't tell us anything about `a :: is`: that's our job. We also still have
+`Hev`, which is our assumption that `find_matching` finds a `y` in `(a :: is)`.
+Running `simpl in Hev` gives us the following:
+
+```
+Hev : (if x + a =? k then Some a else find_matching is k x) = Some y
+```
+
+The result of `find_matching` now depends on whether or not the new element `a`
+adds up to `k`. If it does, then `find_matching` will return `a`, which means
+that `y` is the same as `a`. If not, it must be that `find_matching` finds
+the `y` in the rest of the list, `is`. We're not sure which of the possibilities
+is the case. Fortunately, we don't need to be!
+If we can prove that the `y` that `find_matching` finds is correct regardless
+of whether `a` adds up to `k` or not, we're good to go! To do this,
+we perform case analysis using `destruct`.
+
+Our particular use of `destruct` says: check any possible value for `x + a ?= k`,
+and create an equation `Heq` that tells us what that value is. `?=` returns a boolean
+value, and so `destruct` generates two new goals: one where the function returns `true`,
+and one where it returns `false`. We start with the former. Here's the proof state:
+
+```
+a : nat
+is : list nat
+IHis : forall k x y : nat, find_matching is k x = Some y -> x + y = k
+k, x, y : nat
+Heq : (x + a =? k) = true
+Hev : Some a = Some y
+
+========================= (1 / 1)
+
+x + y = k
+```
+
+There is a new hypothesis: `Heq`. It tells us that we're currently
+considering the case where `?=` evaluates to `true`. Also,
+`Hev` has been considerably simplified: now that we know the condition
+of the `if` expression, we can just replace it with the `then` branch.
+
+Looking at `Hev`, we can see that our prediction was right: `a` is equal to `y`. After all,
+if they weren't, `Some a` wouldn't equal to `Some y`. To make Coq
+take this information into account, we use `injection`. This will create
+a new hypothesis, `a = y`. But if one is equal to the other, why don't we
+just use only one of these variables everywhere? We do exactly that by using
+`subst`, which replaces `a` with `y` everywhere in our proof.
+
+The proof state is now:
+
+```
+is : list nat
+IHis : forall k x y : nat, find_matching is k x = Some y -> x + y = k
+k, x, y : nat
+Heq : (x + y =? k) = true
+
+========================= (1 / 1)
+
+x + y = k
+```
+
+We're close, but there's one more detail to keep in mind. Our goal, `x + y = k`,
+is the __proposition__ that `x + y` is equal to `k`. However, `Heq` tells us
+that the __function__ `?=` evaluates to `true`. These are fundamentally different.
+One talks about mathematical equality, while the other about some function `?=`
+defined somewhere in Coq's standard library. Who knows - maybe there's a bug in
+Coq's implementation! Fortunately, Coq comes with a proof that if two numbers
+are equal according to `?=`, they are mathematically equal. This proof is
+called `eqb_nat_eq`. We tell Coq to use this with `apply`. Our proof goal changes to:
+
+```
+true = (x + y =? k)
+```
+
+This is _almost_ like `Heq`, but flipped. Instead of manually flipping it and using `apply`
+with `Heq`, I let Coq do the rest of the work using `auto`.
+
+Phew! All this for the `true` case of `?=`. Next, what happens if `x + a` does not equal `k`?
+Here's the proof state at this time:
+
+```
+a : nat
+is : list nat
+IHis : forall k x y : nat, find_matching is k x = Some y -> x + y = k
+k, x, y : nat
+Heq : (x + a =? k) = false
+Hev : find_matching is k x = Some y
+
+========================= (1 / 1)
+
+x + y = k
+```
+
+Since `a` was not what it was looking for, `find_matching` moved on to `is`. But hey,
+we're in the inductive case! We are assuming that `find_matching` will work properly
+with the list `is`. Since `find_matching` found its `y` in `is`, this should be all we need!
+We use our induction hypothesis `IHis` with `apply`. `IHis` itself does not know that
+`find_matching` moved on to `is`, so it asks us to prove it. Fortunately, `Hev` tells us
+exactly that, so we use `assumption`, and the proof is complete! Quod erat demonstrandum, QED!
+
+### The Rest of the Owl
+Here are a couple of other properties of `find_matching`. For brevity's sake, I will
+not go through their proofs step-by-step. I find that the best way to understand
+Coq proofs is to actually step through them in the IDE!
+
+First on the list is `find_matching_skip`. Here's the type:
+
+{{< codelines "Coq" "aoc-coq/day1.v" 38 39 >}}
+
+It reads: if we correctly find a number in a small list `is`, we can find that same number
+even if another number is prepended to `is`. That makes sense: _adding_ a number to
+a list doesn't remove whatever we found in it! I used this lemma to prove another,
+`find_matching_works`:
+
+{{< codelines "Coq" "aoc-coq/day1.v" 49 50 >}}
+
+This reads, if there _is_ an element `y` in `is` that adds up to `k` with `x`, then
+`find_matching` will find it. This is an important property. After all, if it didn't
+hold, it would mean that `find_matching` would occasionally fail to find a matching
+number, even though it's there! We can't have that.
+
+Finally, we want to specify what it means for `find_sum`, our solution function, to actually
+work. The naive definition would be:
+
+> Given a list of integers, `find_sum` always finds a pair of numbers that add up to `k`.
+
+Unfortunately, this is not true. What if, for instance, we give `find_sum` an empty list?
+There are no numbers from that list to find and add together. Even a non-empty list
+may not include such a pair! We need a way to characterize valid input lists. I claim
+that all lists from this Advent of Code puzzle are guaranteed to have two numbers that
+add up to our goal, and that these numbers are not equal to each other. In Coq,
+we state this as follows:
+
+{{< codelines "Coq" "aoc-coq/day1.v" 4 5 >}}
+
+This defines a new property, `has_pair t is` (read "`is` has a pair of numbers that add to `t`"),
+which means:
+
+> There are two numbers `n1` and `n2` such that, they are not equal to each other (`n1<>n2`) __and__
+> the number `n1` is an element of `is` (`In n1 is`) __and__
+> the number `n2` is an element of `is` (`In n2 is`) __and__
+> the two numbers add up to `t` (`n1 + n2 = t`).
+
+When making claims about the correctness of our algorithm, we will assume that this
+property holds. Finally, here's the theorem we want to prove:
+
+{{< codelines "Coq" "aoc-coq/day1.v" 64 66 >}}
+
+It reads, "for any total `k` and list `is`, if `is` has a pair of numbers that add to `k`,
+then `find_sum` will return a pair of numbers `x` and `y` that add to `k`".
+There's some nuance here. We hardly reference the `has_pair` property in this definition,
+and for good reason. Our `has_pair` hypothesis only says that there is _at least one_
+pair of numbers in `is` that meets our criteria. However, this pair need not be the only
+one, nor does it need to be the one returned by `find_sum`! However, if we have many pairs,
+we want to confirm that `find_sum` will find one of them. Finally, here is the proof.
+I will not be able to go through it in detail in this post, but I did comment it to
+make it easier to read:
+
+{{< codelines "Coq" "aoc-coq/day1.v" 67 102 >}}
+
+Coq seems happy with it, and so am I! The bug I mentioned earlier popped up on line 96.
+I had accidentally made `find_sum` return `None` if it couldn't find a complement
+for the `x` it encountered. This meant that it never recursed into the remaining
+list `xs`, and thus, the pair was never found at all! It this became impossible
+to prove that `find_some` will return `Some y`, and I had to double back
+and check my definitions.
+
+I hope you enjoyed this post! If you're interested to learn more about Coq, I strongly recommend
+checking out [Software Foundations](https://softwarefoundations.cis.upenn.edu/), a series
+of books on Coq written as comments in a Coq source file! In particular, check out
+[Logical Foundations](https://softwarefoundations.cis.upenn.edu/lf-current/index.html)
+for an introduction to using Coq. Thanks for reading!

content/blog/typesafe_imperative_lang.md

@@ -0,0 +1,476 @@
+---
+title: "A Typesafe Representation of an Imperative Language"
+date: 2020-11-02T01:07:21-08:00
+tags: ["Idris"]
+---
+
+A recent homework assignment for my university's programming languages
+course was to encode the abstract syntax for a small imperative language
+into Haskell data types. The language consisted of very few constructs, and was very much a "toy".
+On the expression side of things, it had three registers (`A`, `B`, and `R`),
+numbers, addition, comparison using "less than", and logical negation. It also
+included a statement for storing the result of an expression into
+a register, `if/else`, and an infinite loop construct with an associated `break` operation.
+A sample program in the language which computes the product of two
+numbers is as follows:
+
+```
+A := 7
+B := 9
+R := 0
+do
+  if A <= 0 then
+    break
+  else
+    R := R + B;
+    A := A + -1;
+  end
+end
+```
+
+The homework notes that type errors may arise in the little imperative language.
+We could, for instance, try to add a boolean to a number: `3 + (1 < 2)`. Alternatively,
+we could try use a number in the condition of an `if/else` expression. A "naive"
+encoding of the abstract syntax would allow for such errors.
+
+However, assuming that registers could only store integers and not booleans, it is fairly easy to
+separate the expression grammar into two nonterminals, yielding boolean
+and integer expressions respectively. Since registers can only store integers,
+the `(:=)` operation will always require an integer expression, and an `if/else`
+statement will always require a boolean expression. A matching Haskell encoding
+would not allow "invalid" programs to compile. That is, the programs would be
+type-correct by construction.
+
+Then, a question arose in the ensuing discussion: what if registers _could_
+contain booleans? It would be impossible to create such a "correct-by-construction"
+representation then, wouldn't it?
+{{< sidenote "right" "haskell-note" "Although I don't know about Haskell," >}}
+I am pretty certain that a similar encoding in Haskell is possible. However,
+Haskell wasn't originally created for that kind of abuse of its type system,
+so it would probably not look very good.
+{{< /sidenote >}} I am sure that it _is_ possible to do this
+in Idris, a dependently typed programming language. In this post I will
+talk about how to do that.
+
+### Registers and Expressions
+Let's start by encoding registers. Since we only have three registers, we
+can encode them using a simple data type declaration, much the same as we
+would in Haskell:
+
+{{< codelines "Idris" "typesafe-imperative/TypesafeImp.idr" 1 1 >}}
+
+Now that registers can store either integers or booleans (and only those two),
+we need to know which one is which. For this purpose, we can declare another
+data type:
+
+{{< codelines "Idris" "typesafe-imperative/TypesafeImp.idr" 3 3 >}}
+
+At any point in the (hypothetical) execution of our program, each
+of the registers will have a type, either boolean or integer. The
+combined state of the three registers would then be the combination
+of these three states; we can represent this using a 3-tuple:
+
+{{< codelines "Idris" "typesafe-imperative/TypesafeImp.idr" 5 6 >}}
+
+Let's say that the first element of the tuple will be the type of the register
+`A`, the second the type of `B`, and the third the type of `R`. Then,
+we can define two helper functions, one for retrieving the type of
+a register, and one for changing it:
+
+{{< codelines "Idris" "typesafe-imperative/TypesafeImp.idr" 8 16 >}}
+
+Now, it's time to talk about expressions. We know now that an expression
+can evaluate to either a boolean or an integer value (because a register
+can contain either of those types of values). Perhaps we can specify
+the type that an expression evaluates to in the expression's own type:
+`Expr IntTy` would evaluate to integers, and `Expr BoolTy` would evaluate
+to booleans. Then, we could have constructors as follows:
+
+```Idris
+Lit : Int -> Expr IntTy
+Not : Expr BoolTy -> Expr BoolTy
+```
+
+Sounds good! But what about loading a register?
+
+```Idris
+Load : Reg -> Expr IntTy -- no; what if the register is a boolean?
+Load : Reg -> Expr BoolTy -- no; what if the register is an integer?
+Load : Reg -> Expr a -- no; a register access can't be either!
+```
+
+The type of an expression that loads a register depends on the current
+state of the program! If we last stored an integer into a register,
+then loading from that register would give us an integer. But if we
+last stored a boolean into a register, then reading from it would
+give us a boolean. Our expressions need to be aware of the current
+types of each register. To do so, we add the state as a parameter to
+our `Expr` type. This would lead to types like the following:
+
+```Idris
+-- An expression that produces a boolean when all the registers
+-- are integers.
+Expr (IntTy, IntTy, IntTy) BoolTy
+
+-- An expression that produces an integer when A and B are integers,
+-- and R is a boolean.
+Expr (IntTy, IntTy, BoolTy) IntTy
+```
+
+In Idris, the whole definition becomes:
+
+{{< codelines "Idris" "typesafe-imperative/TypesafeImp.idr" 18 23 >}}
+
+The only "interesting" constructor is `Load`, which, given a register `r`,
+creates an expression that has `r`'s type in the current state `s`.
+
+### Statements
+Statements are a bit different. Unlike expressions, they don't evaluate to
+anything; rather, they do something. That "something" may very well be changing
+the current state. We could, for instance, set `A` to be a boolean, while it was
+previously an integer. This suggests equipping our `Stmt` type with two
+arguments: the initial state (before the statement's execution), and the final
+state (after the statement's execution). This would lead to types like this:
+
+```Idris
+-- Statement that, when run while all registers contain integers,
+-- terminates with registers B and R having been assigned boolean values.
+Stmt (IntTy, IntTy, IntTy) (IntTy, BoolTy, BoolTy)
+```
+
+However, there's a problem with `loop` and `break`. When we run a loop,
+we will require that the state at the end of one iteration is the
+same as the state at its beginning. Otherwise, it would be possible
+for a loop to keep changing the types of registers every iteration,
+and it would become impossible for us to infer the final state
+without actually running the program. In itself, this restriction
+isn't a problem; most static type systems require both branches
+of an `if/else` expression to be of the same type for a similar
+reason. The problem comes from the interaction with `break`.
+
+By itself, the would-be type of `break` seems innocent enough. It
+doesn't change any registers, so we could call it `Stmt s s`.
+But consider the following program:
+
+```
+A := 0
+B := 0
+R := 0
+do
+  if 5 <= A then
+    B := 1 <= 1
+    break
+    B := 0
+  else
+    A := A + 1
+  end
+end
+```
+
+The loop starts with all registers having integer values.
+As per our aforementioned loop requirement, the body
+of the loop must terminate with all registers _still_ having
+integer values. For the first five iterations that's exactly
+what will happen. However, after we increment `A` the fifth time,
+we will set `B` to a boolean value -- using a valid statement --
+and then `break`. The `break` statement will be accepted by
+the typechecker, and so will the whole `then` branch. After all,
+it seems as though we reset `B` back to an integer value.
+But that won't be the case. We will have jumped to the end
+of the loop, where we are expected to have an all-integer type,
+which we will not have.
+
+The solution I came up with to address this issue was to
+add a _third_ argument to `Stmt`, which contains the "context"
+type. That is, it contains the type of the innermost loop surrounding
+the statement. A `break` statement would only be permissible
+if the current type matches the loop type. With this, we finally
+write down a definition of `Stmt`:
+
+{{< codelines "Idris" "typesafe-imperative/TypesafeImp.idr" 26 30 >}}
+
+The `Store` constructor takes a register `r` and an expression producing some type `t` in state `s`.
+From these, it creates a statement that starts in `s`, and finishes
+in a state similar to `s`, but with `r` now having type `t`. The loop
+type `l` remains unaffected and unused; we are free to assign any register
+any value.
+
+The `If` constructor takes a condition `Expr`, which starts in state `s` and _must_ produce
+a boolean. It also takes two programs (sequences of statements), each of which
+starts in `s` and finishes in another state `n`. This results in
+a statement that starts in state `s`, and finishes in state `n`. Conceptually,
+each branch of the `if/else` statement must result in the same final state (in terms of types);
+otherwise, we wouldn't know which of the states to pick when deciding the final
+state of the `If` itself. As with `Store`, the loop type `l` is untouched here.
+Individual statements are free to modify the state however they wish.
+
+The `Loop` constructor is very restrictive. It takes a single program (the sequence
+of instructions that it will be repeating). As we discussed above, this program
+must start _and_ end in the same state `s`. Furthermore, this program's loop
+type must also be `s`, since the loop we're constructing will be surrounding the
+program. The resulting loop itself still has an arbitrary loop type `l`, since
+it doesn't surround itself.
+
+Finally, `Break` can only be constructed when the loop state matches the current
+state. Since we'll be jumping to the end of the innermost loop, the final state
+is also the same as the loop state. 
+
+These are all the constructors we'll be needing. It's time to move on to
+whole programs!
+
+### Programs
+A program is simply a list of statements. However, we can't use a regular Idris list,
+because a regular list wouldn't be able to represent the relationship between
+each successive statement. In our program, we want the final state of one
+statement to be the initial state of the following one, since they'll
+be executed in sequence. To represent this, we have to define our own
+list-like GADT. The definition of the type turns out fairly straightforward:
+
+{{< codelines "Idris" "typesafe-imperative/TypesafeImp.idr" 32 34 >}}
+
+The `Nil` constructor represents an empty program (much like the built-in `Nil` represents an empty list).
+Since no actions are done, it creates a `Prog` that starts and ends in the same state: `s`.
+The `(::)` constructor, much like the built-in `(::)` constructor, takes a statement
+and another program. The statement begins in state `s` and ends in state `n`; the program after
+that statement must then start in state `n`, and end in some other state `m`.
+The combination of the statement and the program starts in state `s`, and finishes in state `m`.
+Thus, `(::)` yields `Prog s m`. None of the constructors affect the loop type `l`: we
+are free to sequence any statements that we want, and it is impossible for us
+to construct statements using `l` that cause runtime errors.
+
+This should be all! Let's try out some programs.
+
+### Trying it Out
+The following (type-correct) program compiles just fine:
+
+{{< codelines "Idris" "typesafe-imperative/TypesafeImp.idr" 36 47 >}}
+
+First, it loads a boolean into register `A`; then,
+inside the `if/else` statement, it stores an integer into `A`. Finally,
+it stores another integer into `B`, and adds them into `R`. Even though
+`A` was a boolean at first, the type checker can deduce that it
+was reset back to an integer after the `if/else`, and the program is accepted.
+On the other hand, had we forgotten to set `A` to a boolean first:
+
+```Idris
+  [ If (Load A)
+    [ Store A (Lit 1) ]
+    [ Store A (Lit 2) ]
+  , Store B (Lit 2)
+  , Store R (Add (Load A) (Load B))
+  ]
+```
+
+We would get a type error:
+
+```
+Type mismatch between getRegTy A (IntTy, IntTy, IntTy) and BoolTy
+```
+
+The type of register `A` (that is, `IntTy`) is incompatible
+with `BoolTy`. Our `initialState` says that `A` starts out as
+an integer, so it can't be used in an `if/else` right away!
+Similar errors occur if we make one of the branches of
+the `if/else` empty, or if we set `B` to a boolean.
+
+We can also encode the example program from the beginning
+of this post:
+
+{{< codelines "Idris" "typesafe-imperative/TypesafeImp.idr" 49 61 >}}
+
+This program compiles just fine, too! It is a little reminiscent of
+the program we used to demonstrate how `break` could break things
+if we weren't careful. So, let's go ahead and try `break` in an invalid
+state:
+
+```Idris
+  [ Store A (Lit 7)
+  , Store B (Lit 9)
+  , Store R (Lit 0)
+  , Loop
+    [ If (Load A `Leq` Lit 0)
+      [ Store B (Lit 1 `Leq` Lit 1), Break, Store B (Lit 0) ]
+      [ Store R (Load R `Add` Load B)
+      , Store A (Load A `Add` Lit (-1))
+      ]
+    ]
+  ]
+```
+
+Again, the type checker complains:
+
+```
+Type mismatch between IntTy and BoolTy
+```
+
+And so, we have an encoding of our language that allows registers to
+be either integers or booleans, while still preventing
+type-incorrect programs!
+
+### Building an Interpreter
+A good test of such an encoding is the implementation
+of an interpreter. It should be possible to convince the
+typechecker that our interpreter doesn't need to
+handle type errors in the toy language, since they
+cannot occur.
+
+Let's start with something simple. First of all, suppose
+we have an expression of type `Expr InTy`. In our toy
+language, it produces an integer. Our interpreter, then,
+will probably want to use Idris' type `Int`. Similarly,
+an expression of type `Expr BoolTy` will produce a boolean
+in our toy language, which in Idris we can represent using
+the built-in `Bool` type. Despite the similar naming, though,
+there's no connection between Idris' `Bool` and our own `BoolTy`.
+We need to define a conversion from our own types -- which are
+values of type `Ty` -- into Idris types that result from evaluating
+expressions. We do so as follows:
+
+{{< codelines "Idris" "typesafe-imperative/TypesafeImp.idr" 63 65 >}}
+
+Similarly, we want to convert our `TypeState` (a tuple describing the _types_
+of our registers) into a tuple that actually holds the values of each
+register, which we will call `State`. The value of each register at
+any point depends on its type. My first thought was to define
+`State` as a function from `TypeState` to an Idris `Type`:
+
+```Idris
+State : TypeState -> Type
+State (a, b, c) = (repr a, repr b, repr c)
+```
+
+Unfortunately, this doesn't quite cut it. The problem is that this
+function technically doesn't give Idris any guarantees that `State`
+will be a tuple. The most Idris knows is that `State` will be some
+`Type`, which could be `Int`, `Bool`, or anything else! This
+becomes a problem when we try to pattern match on states to get
+the contents of a particular register. Instead, we have to define
+a new data type:
+
+{{< codelines "Idris" "typesafe-imperative/TypesafeImp.idr" 67 68 >}}
+
+In this snippet, `State` is still a (type level) function from `TypeState` to `Type`.
+However, by using a GADT, we guarantee that there's only one way to construct
+a `State (a,b,c)`: using a corresponding tuple. Now, Idris will accept our
+pattern matching:
+
+{{< codelines "Idris" "typesafe-imperative/TypesafeImp.idr" 70 78 >}}
+
+The `getReg` function will take out the value of the corresponding
+register, returning `Int` or `Bool` depending on the `TypeState`.
+What's important is that if the `TypeState` is known, then so
+is the type of `getReg`: no `Either` is involved here, and we
+can directly use the integer or boolean stored in the
+register. This is exactly what we do:
+
+{{< codelines "Idris" "typesafe-imperative/TypesafeImp.idr" 80 85 >}}
+
+This is pretty concise. Idris knows that `Lit i` is of type `Expr IntTy`,
+and it knows that `repr IntTy = Int`, so it also knows that
+`eval (Lit i)` produces an `Int`. Similarly, we wrote
+`Reg r` to have type `Expr s (getRegTy r s)`. Since `getReg`
+returns `repr (getRegTy r s)`, things check out here, too.
+A similar logic applies to the rest of the cases.
+
+The situation with statements is somewhat different. As we said, a statement
+doesn't return a value; it changes state. A good initial guess would
+be that to evaluate a statement that starts in state `s` and terminates in state `n`,
+we would take as input `State s` and return `State n`. However, things are not
+quite as simple, thanks to `Break`. Not only does `Break` require
+special case logic to return control to the end of the `Loop`, but
+it also requires some additional consideration: in a statement
+of type `Stmt l s n`, evaluating `Break` can return `State l`.
+
+To implement this, we'll use the `Either` type. The `Left` constructor
+will be contain the state at the time of evaluating a `Break`,
+and will indicate to the interpreter that we're breaking out of a loop.
+On the other hand, the `Right` constructor will contain the state
+as produced by all other statements, which would be considered
+{{< sidenote "right" "left-right-note" "the \"normal\" case." >}}
+We use <code>Left</code> for the "abnormal" case because of
+Idris' (and Haskell's) convention to use it as such. For
+instance, the two languages define a <code>Monad</code>
+instance for <code>Either a</code> where <code>(>>=)</code>
+behaves very much like it does for <code>Maybe</code>, with
+<code>Left</code> being treated as <code>Nothing</code>,
+and <code>Right</code> as <code>Just</code>. We will
+use this instance to clean up some of our computations.
+{{< /sidenote >}} Note that this doesn't indicate an error:
+we need to represent the two states (breaking out of a loop
+and normal execution) to define our language's semantics.
+
+{{< codelines "Idris" "typesafe-imperative/TypesafeImp.idr" 88 95 >}}
+
+First, note the type. We return an `Either` value, which will
+contain `State l` (in the `Left` constructor) if a `Break`
+was evaluated, and `State n` (in the `Right` constructor)
+if execution went on without breaking.
+
+The `Store` case is rather simple. We use `setReg` to update the result
+of the register `r` with the result of evaluating `e`. Because
+a store doesn't cause us to start breaking out of a loop,
+we use `Right` to wrap the new state.
+
+The `If` case is also rather simple. Its condition is guaranteed
+to evaluate to a boolean, so it's sufficient for us to use
+Idris' `if` expression. We use the `prog` function here, which
+implements the evaluation of a whole program. We'll get to it
+momentarily.
+
+`Loop` is the most interesting case. We start by evaluating
+the program `p` serving as the loop body. The result of this
+computation will be either a state after a break,
+held in `Left`, or as the normal execution state, held
+in `Right`. The `(>>=)` operation will do nothing in
+the first case, and feed the resulting (normal) state
+to `stmt (Loop p)` in the second case. This is exactly
+what we want: if we broke out of the current iteration
+of the loop, we shouldn't continue on to the next iteration.
+At the end of evaluating both `p` and the recursive call to
+`stmt`, we'll either have exited normally, or via breaking
+out. We don't want to continue breaking out further,
+so we return the final state wrapped in `Right` in both cases.
+Finally, `Break` returns the current state wrapped in `Left`,
+beginning the process of breaking out.
+
+The task of `prog` is simply to sequence several statements
+together. The monadic bind operator, `(>>=)`, is again perfect
+for this task, since it "stops" when it hits a `Left`, but
+continues otherwise. This is the implementation:
+
+{{< codelines "Idris" "typesafe-imperative/TypesafeImp.idr" 97 99 >}}
+
+Awesome! Let's try it out, shall we? I defined a quick `run` function
+as follows:
+
+{{< codelines "Idris" "typesafe-imperative/TypesafeImp.idr" 101 102 >}}
+
+We then have:
+
+```
+*TypesafeImp> run prodProg (MkState (0,0,0))
+MkState (0, 9, 63) : State (IntTy, IntTy, IntTy)
+```
+
+This seems correct! The program multiplies seven by nine,
+and stops when register `A` reaches zero. Our test program
+runs, too:
+
+```
+*TypesafeImp> run testProg (MkState (0,0,0))
+MkState (1, 2, 3) : State (IntTy, IntTy, IntTy)
+```
+
+This is the correct answer: `A` ends up being set to
+`1` in the `then` branch of the conditional statement,
+`B` is set to 2 right after, and `R`, the sum of `A`
+and `B`, is rightly `3`.
+
+As you can see, we didn't have to write any error handling
+code! This is because the typechecker _knows_ that type errors
+aren't possible: our programs are guaranteed to be
+{{< sidenote "right" "termination-note" "type correct." >}}
+Our programs <em>aren't</em> guaranteed to terminate:
+we're lucky that Idris' totality checker is turned off by default.
+{{< /sidenote >}} This was a fun exercise, and I hope you enjoyed reading along!
+I hope to see you in my future posts.

layouts/shortcodes/gt_assumption.html

@@ -0,0 +1,9 @@
+{{ $n := .Page.Scratch.Get "gt-assumption-count" }}
+{{ $newN := add 1 (int $n) }}
+{{ .Page.Scratch.Set "gt-assumption-count" $newN }}
+{{ .Page.Scratch.SetInMap "gt-assumptions" (.Get 0) $newN }}
+<div class="assumption">
+    <span id="gt-assumption-{{ .Get 0 }}" class="assumption-number">
+        Assumption {{ $newN }} ({{ .Get 1 }}).
+    </span> {{ .Inner }}
+</div>

layouts/shortcodes/gt_css.html

@@ -0,0 +1,2 @@
+{{ $style := resources.Get "scss/gametheory.scss" | resources.ToCSS | resources.Minify }}
+<link rel="stylesheet" href="{{ $style.Permalink }}">

layouts/shortcodes/gt_link.html

@@ -0,0 +1 @@
+<a href="#gt-assumption-{{ .Get 0 }}">assumption {{ index (.Page.Scratch.Get "gt-assumptions") (.Get 0) }}</a>

themes/vanilla/assets/scss/code.scss

@@ -5,6 +5,16 @@ $code-color-keyword: black;
 $code-color-type: black;
 $code-color-comment: grey;
 
+.highlight-label {
+    padding: 0.25rem 0.5rem 0.25rem 0.5rem;
+    border: $code-border;
+    border-bottom: none;
+
+    a {
+        font-family: $font-code;
+    }
+}
+
 code {
   font-family: $font-code;
   background-color: $code-color;
@@ -61,6 +71,10 @@ pre code {
     .hl {
         display: block;
         background-color: #fffd99; 
+
+        .lnt::before {
+            content: "*";
+        }
     }
 }
 

themes/vanilla/assets/scss/search.scss

@@ -0,0 +1,94 @@
+@import "variables.scss";
+@import "mixins.scss";
+
+$search-input-padding: 0.5rem;
+$search-element-padding: 0.5rem 1rem 0.5rem 1rem;
+
+@mixin green-shadow {
+    box-shadow: 0px 0px 5px rgba($primary-color, 0.7);
+}
+
+.stork-input-wrapper {
+    display: flex;
+    flex-direction: row;
+    flex-wrap: wrap;
+}
+
+input.stork-input {
+    @include bordered-block;
+    font-family: $font-body;
+    padding: $search-input-padding;
+
+    &:active, &:focus {
+        @include green-shadow;
+        border-color: $primary-color;
+    }
+
+    flex-grow: 1;
+}
+
+.stork-close-button {
+    @include bordered-block;
+    font-family: $font-body;
+    padding: $search-input-padding;
+
+    background-color: $code-color;
+    padding-left: 1.5rem;
+    padding-right: 1.5rem;
+
+    border-left: none;
+    border-top-left-radius: 0;
+    border-bottom-left-radius: 0;
+}
+
+.stork-output-visible {
+    @include bordered-block;
+
+    border-top: none;
+}
+
+.stork-result, .stork-message, .stork-attribution {
+    padding: $search-element-padding;
+}
+
+.stork-message:not(:last-child), .stork-result  {
+    border-bottom: $standard-border;
+}
+
+.stork-results {
+    margin: 0;
+    padding: 0;
+}
+
+.stork-result {
+    list-style: none;
+
+    &.selected {
+        background-color: $code-color;
+    }
+
+    a:hover {
+        color: black;
+    }
+}
+
+.stork-title, .stork-excerpt {
+    margin: 0;
+}
+
+.stork-excerpt {
+    white-space: nowrap;
+    overflow: hidden;
+    text-overflow: ellipsis;
+}
+
+.stork-title {
+    font-family: $font-heading;
+    font-size: 1.4rem;
+    text-align: left;
+    width: 100%;
+}
+
+.stork-highlight {
+    background-color: lighten($primary-color, 30%);
+}

themes/vanilla/assets/scss/style.scss

@@ -233,3 +233,10 @@ figure {
 .twitter-tweet {
     margin: auto;
 }
+
+.draft-warning {
+    @include bordered-block;
+    padding: 0.5rem;
+    background-color: #ffee99;
+    border-color: #f5c827;
+}

themes/vanilla/layouts/_default/baseof.toml

@@ -0,0 +1 @@
+{{- block "main" . }}{{- end }}

themes/vanilla/layouts/_default/list.toml.toml

@@ -0,0 +1,12 @@
+[input]
+base_directory = "content/"
+title_boost = "Large"
+files = [
+    {{ range $index , $e := .Site.RegularPages }}{{ if $index }}, {{end}}{ filetype = "PlainText", contents = {{ $e.Plain | jsonify }}, title = {{ $e.Title | jsonify }}, url = {{ $e.Permalink | jsonify }} }
+    {{ end }}
+]
+
+[output]
+filename = "index.st"
+excerpts_per_result = 2
+displayed_results_count = 5

themes/vanilla/layouts/_default/single.toml

@@ -0,0 +1,3 @@
+{{ define "main" }}
+{{ .Content }}
+{{ end }}

themes/vanilla/layouts/blog/single.html

@@ -18,6 +18,15 @@
         </div>
     </div>
     {{ end }}
+
+    {{ if .Draft }}
+    <div class="draft-warning">
+        <em>Warning!</em> This post is a draft. At best, it may contain grammar mistakes;
+        at worst, it can include significant errors and bugs. Please
+        use your best judgement!
+    </div>
+    {{ end }}
+
     {{ .Content }}
 </div>
 {{ end }}

themes/vanilla/layouts/index.html

@@ -1,10 +1,22 @@
 {{ define "main" }}
 {{ .Content }}
 
+<p>
+    <div class="stork-wrapper">
+        <div class="stork-input-wrapper">
+            <input class="stork-input" data-stork="blog" placeholder="Search (requires JavaScript)"/>
+        </div>
+        <div class="stork-output" data-stork="blog-output"></div>
+    </div>
+</p>
+
 Recent posts:
 <ul class="post-list">
     {{ range first 10 (where (where .Site.Pages.ByDate.Reverse "Section" "blog") ".Kind" "!=" "section") }}
     {{ partial "post.html" . }}
     {{ end }}
 </ul>
+
+<script src="https://files.stork-search.net/stork.js"></script>
+<script>stork.register("blog", "/index.st");</script>
 {{ end }}

themes/vanilla/layouts/partials/head.html

@@ -11,11 +11,13 @@
     {{ $style := resources.Get "scss/style.scss" | resources.ToCSS | resources.Minify }}
     {{ $sidenotes := resources.Get "scss/sidenotes.scss" | resources.ToCSS | resources.Minify }}
     {{ $code := resources.Get "scss/code.scss" | resources.ToCSS | resources.Minify }}
+    {{ $search := resources.Get "scss/search.scss" | resources.ToCSS | resources.Minify }}
     {{ $icon := resources.Get "img/favicon.png" }}
     {{- partial "sidenotes.html" . -}}
     <link rel="stylesheet" href="{{ $style.Permalink }}" media="screen">
     <link rel="stylesheet" href="{{ $sidenotes.Permalink }}" media="screen">
     <link rel="stylesheet" href="{{ $code.Permalink }}" media="screen">
+    <link rel="stylesheet" href="{{ $search.Permalink }}" media="screen">
     <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.11.1/dist/katex.min.css" integrity="sha384-zB1R0rpPzHqg7Kpt0Aljp8JPLqbXI3bhnPWROx27a9N0Ll6ZP/+DiW/UqRcLbRjq" crossorigin="anonymous" media="screen">
     <link rel="icon" type="image/png" href="{{ $icon.Permalink }}">
 

themes/vanilla/layouts/shortcodes/codelines.html

@@ -11,4 +11,8 @@
 {{ else }}
 {{ .Scratch.Set "opts" "" }}
 {{ end }}
-{{ highlight (delimit $v "\n") (.Get 0) (printf "linenos=table,linenostart=%d%s" (.Get 2) (.Scratch.Get "opts")) }}
+<div class="highlight-group">
+    <div class="highlight-label">From <a href="https://dev.danilafe.com/Web-Projects/blog-static/src/branch/master/code/{{ .Get 1 }}">{{ path.Base (.Get 1) }}</a>,
+        {{ if eq (.Get 2) (.Get 3) }}line {{ .Get 2 }}{{ else }} lines {{ .Get 2 }} through {{ .Get 3 }}{{ end }}</div>
+    {{ highlight (delimit $v "\n") (.Get 0) (printf "linenos=table,linenostart=%d%s" (.Get 2) (.Scratch.Get "opts")) }}
+</div>