Edit and publish second Coq Dawn article

Add illustrations about evaluation chains
Remove undercore from refl constructor to avoid KaTeX errors
2021-12-02 18:29:47 -08:00 · 2021-12-02 17:41:36 -08:00 · 2021-11-28 19:34:57 -08:00 · 2021-11-28 17:33:04 -08:00 · 2021-11-28 16:50:28 -08:00 · 2021-11-28 16:46:56 -08:00
29 changed files with 1995 additions and 7 deletions
--- a/assets/scss/donate.scss
+++ b/assets/scss/donate.scss
@@ -17,12 +17,32 @@
            border-bottom-right-radius: 0;
            padding-left: 0.5em;
            padding-right: 0.5rem;
+
+            @include below-container-width {
+                @include bordered-block;
+                text-align: center;
+                border-bottom: none;
+                border-bottom-left-radius: 0;
+                border-bottom-right-radius: 0;
+            }
        }

        &:last-child {
            @include bordered-block;
            border-top-left-radius: 0;
            border-bottom-left-radius: 0;
+
+            @include below-container-width {
+                @include bordered-block;
+                border-top-left-radius: 0;
+                border-top-right-radius: 0;
+            }
+        }
+    }
+
+    tr {
+        @include below-container-width {
+            margin-bottom: 0.5rem;
        }
    }

--- a/code/dawn/Dawn.v
+++ b/code/dawn/Dawn.v
@@ -0,0 +1,179 @@
+Require Import Coq.Lists.List.
+From Ltac2 Require Import Ltac2.
+
+Inductive intrinsic :=
+  | swap
+  | clone
+  | drop
+  | quote
+  | compose
+  | apply.
+
+Inductive expr :=
+  | e_int (i : intrinsic)
+  | e_quote (e : expr)
+  | e_comp (e1 e2 : expr).
+
+Definition e_compose (e : expr) (es : list expr) := fold_left e_comp es e.
+
+Inductive IsValue : expr -> Prop :=
+  | Val_quote : forall {e : expr}, IsValue (e_quote e).
+
+Definition value := { v : expr & IsValue v }.
+Definition value_stack := list value.
+
+Definition v_quote (e : expr) := existT IsValue (e_quote e) Val_quote.
+
+Inductive Sem_int : value_stack -> intrinsic -> value_stack -> Prop :=
+  | Sem_swap : forall (v v' : value) (vs : value_stack), Sem_int (v' :: v :: vs) swap (v :: v' :: vs)
+  | Sem_clone : forall (v : value) (vs : value_stack), Sem_int (v :: vs) clone (v :: v :: vs)
+  | Sem_drop : forall (v : value) (vs : value_stack), Sem_int (v :: vs) drop vs
+  | Sem_quote : forall (v : value) (vs : value_stack), Sem_int (v :: vs) quote ((v_quote (projT1 v)) :: vs)
+  | Sem_compose : forall (e e' : expr) (vs : value_stack), Sem_int (v_quote e' :: v_quote e :: vs) compose (v_quote (e_comp e e') :: vs)
+  | Sem_apply : forall (e : expr) (vs vs': value_stack), Sem_expr vs e vs' -> Sem_int (v_quote e :: vs) apply vs'
+
+with Sem_expr : value_stack -> expr -> value_stack -> Prop :=
+  | Sem_e_int : forall (i : intrinsic) (vs vs' : value_stack), Sem_int vs i vs' -> Sem_expr vs (e_int i) vs'
+  | Sem_e_quote : forall (e : expr) (vs : value_stack), Sem_expr vs (e_quote e) (v_quote e :: vs)
+  | Sem_e_comp : forall (e1 e2 : expr) (vs1 vs2 vs3 : value_stack),
+      Sem_expr vs1 e1 vs2 -> Sem_expr vs2 e2 vs3 -> Sem_expr vs1 (e_comp e1 e2) vs3.
+
+Definition false : expr := e_quote (e_int drop).
+Definition false_v : value := v_quote (e_int drop).
+
+Definition true : expr := e_quote (e_comp (e_int swap) (e_int drop)).
+Definition true_v : value := v_quote (e_comp (e_int swap) (e_int drop)).
+
+Theorem false_correct : forall (v v' : value) (vs : value_stack), Sem_expr (v' :: v :: vs) (e_comp false (e_int apply)) (v :: vs).
+Proof.
+  intros v v' vs.
+  eapply Sem_e_comp.
+  - apply Sem_e_quote.
+  - apply Sem_e_int. apply Sem_apply. apply Sem_e_int. apply Sem_drop.
+Qed.
+
+Theorem true_correct : forall (v v' : value) (vs : value_stack), Sem_expr (v' :: v :: vs) (e_comp true (e_int apply)) (v' :: vs).
+Proof.
+  intros v v' vs.
+  eapply Sem_e_comp.
+  - apply Sem_e_quote.
+  - apply Sem_e_int. apply Sem_apply. eapply Sem_e_comp.
+    * apply Sem_e_int. apply Sem_swap.
+    * apply Sem_e_int. apply Sem_drop.
+Qed.
+
+Definition or : expr := e_comp (e_int clone) (e_int apply).
+
+Theorem or_false_v : forall (v : value) (vs : value_stack), Sem_expr (false_v :: v :: vs) or (v :: vs).
+Proof with apply Sem_e_int.
+  intros v vs.
+  eapply Sem_e_comp...
+  - apply Sem_clone.
+  - apply Sem_apply... apply Sem_drop.
+Qed.
+
+Theorem or_true : forall (v : value) (vs : value_stack), Sem_expr (true_v :: v :: vs) or (true_v :: vs).
+Proof with apply Sem_e_int.
+  intros v vs.
+  eapply Sem_e_comp...
+  - apply Sem_clone...
+  - apply Sem_apply. eapply Sem_e_comp...
+    * apply Sem_swap.
+    * apply Sem_drop.
+Qed.
+
+Definition or_false_false := or_false_v false_v.
+Definition or_false_true := or_false_v true_v.
+Definition or_true_false := or_true false_v.
+Definition or_true_true := or_true true_v.
+
+Fixpoint quote_n (n : nat) :=
+  match n with
+  | O => e_int quote
+  | S n' => e_compose (quote_n n') (e_int swap :: e_int quote :: e_int swap :: e_int compose :: nil)
+  end.
+
+Theorem quote_2_correct : forall (v1 v2 : value) (vs : value_stack),
+    Sem_expr (v2 :: v1 :: vs) (quote_n 1) (v_quote (e_comp (projT1 v1) (projT1 v2)) :: vs).
+Proof with apply Sem_e_int.
+  intros v1 v2 vs. simpl.
+  repeat (eapply Sem_e_comp)...
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_compose.
+Qed.
+
+Theorem quote_3_correct : forall (v1 v2 v3 : value) (vs : value_stack),
+  Sem_expr (v3 :: v2 :: v1 :: vs) (quote_n 2) (v_quote (e_comp (projT1 v1) (e_comp (projT1 v2) (projT1 v3))) :: vs).
+Proof with apply Sem_e_int.
+  intros v1 v2 v3 vs. simpl.
+  repeat (eapply Sem_e_comp)...
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_compose.
+  - apply Sem_swap.
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_compose.
+Qed.
+
+Ltac2 rec solve_basic () := Control.enter (fun _ =>
+  match! goal with
+  | [|- Sem_int ?vs1 swap ?vs2] => apply Sem_swap
+  | [|- Sem_int ?vs1 clone ?vs2] => apply Sem_clone
+  | [|- Sem_int ?vs1 drop ?vs2] => apply Sem_drop
+  | [|- Sem_int ?vs1 quote ?vs2] => apply Sem_quote
+  | [|- Sem_int ?vs1 compose ?vs2] => apply Sem_compose
+  | [|- Sem_int ?vs1 apply ?vs2] => apply Sem_apply
+  | [|- Sem_expr ?vs1 (e_comp ?e1 ?e2) ?vs2] => eapply Sem_e_comp; solve_basic ()
+  | [|- Sem_expr ?vs1 (e_int ?e) ?vs2] => apply Sem_e_int; solve_basic ()
+  | [|- Sem_expr ?vs1 (e_quote ?e) ?vs2] => apply Sem_e_quote
+  | [_ : _ |- _] => ()
+  end).
+
+Theorem quote_2_correct' : forall (v1 v2 : value) (vs : value_stack),
+    Sem_expr (v2 :: v1 :: vs) (quote_n 1) (v_quote (e_comp (projT1 v1) (projT1 v2)) :: vs).
+Proof. intros. simpl. solve_basic (). Qed.
+
+Theorem quote_3_correct' : forall (v1 v2 v3 : value) (vs : value_stack),
+  Sem_expr (v3 :: v2 :: v1 :: vs) (quote_n 2) (v_quote (e_comp (projT1 v1) (e_comp (projT1 v2) (projT1 v3))) :: vs).
+Proof. intros. simpl. solve_basic (). Qed.
+
+Definition rotate_n (n : nat) := e_compose (quote_n n) (e_int swap :: e_int quote :: e_int compose :: e_int apply :: nil).
+
+Lemma eval_value : forall (v : value) (vs : value_stack),
+  Sem_expr vs (projT1 v) (v :: vs).
+Proof.
+  intros v vs.
+  destruct v. destruct i.
+  simpl. apply Sem_e_quote.
+Qed.
+
+Theorem rotate_3_correct : forall (v1 v2 v3 : value) (vs : value_stack),
+  Sem_expr (v3 :: v2 :: v1 :: vs) (rotate_n 1) (v1 :: v3 :: v2 :: vs).
+Proof.
+  intros. unfold rotate_n. simpl. solve_basic ().
+  repeat (eapply Sem_e_comp); apply eval_value.
+Qed.
+
+Theorem rotate_4_correct : forall (v1 v2 v3 v4 : value) (vs : value_stack),
+  Sem_expr (v4 :: v3 :: v2 :: v1 :: vs) (rotate_n 2) (v1 :: v4 :: v3 :: v2 :: vs).
+Proof.
+  intros. unfold rotate_n. simpl. solve_basic ().
+  repeat (eapply Sem_e_comp); apply eval_value.
+Qed.
+
+Theorem e_comp_assoc : forall (e1 e2 e3 : expr) (vs vs' : value_stack),
+  Sem_expr vs (e_comp e1 (e_comp e2 e3)) vs' <-> Sem_expr vs (e_comp (e_comp e1 e2) e3) vs'.
+Proof.
+  intros e1 e2 e3 vs vs'.
+  split; intros Heval.
+  - inversion Heval; subst. inversion H4; subst.
+    eapply Sem_e_comp. eapply Sem_e_comp. apply H2. apply H3. apply H6.
+  - inversion Heval; subst. inversion H2; subst.
+    eapply Sem_e_comp. apply H3. eapply Sem_e_comp. apply H6. apply H4.
+Qed.
--- a/code/dawn/DawnEval.v
+++ b/code/dawn/DawnEval.v
@@ -0,0 +1,254 @@
+Require Import Coq.Lists.List.
+Require Import DawnV2.
+Require Import Coq.Program.Equality.
+From Ltac2 Require Import Ltac2.
+
+Inductive step_result :=
+  | err
+  | middle (e : expr) (s : value_stack)
+  | final (s : value_stack).
+
+Fixpoint eval_step (s : value_stack) (e : expr) : step_result :=
+  match e, s with
+  | e_int swap, v' :: v :: vs => final (v :: v' :: vs)
+  | e_int clone, v :: vs => final (v :: v :: vs)
+  | e_int drop, v :: vs => final vs
+  | e_int quote, v :: vs => final (v_quote (value_to_expr v) :: vs)
+  | e_int compose, (v_quote v2) :: (v_quote v1) :: vs => final (v_quote (e_comp v1 v2) :: vs)
+  | e_int apply, (v_quote v1) :: vs => middle v1 vs
+  | e_quote e', vs => final (v_quote e' :: vs)
+  | e_comp e1 e2, vs =>
+      match eval_step vs e1 with
+      | final vs' => middle e2 vs'
+      | middle e1' vs' => middle (e_comp e1' e2) vs'
+      | err => err
+      end
+  | _, _ => err
+  end.
+
+Theorem eval_step_correct : forall (e : expr) (vs vs' : value_stack), Sem_expr vs e vs' ->
+  (eval_step vs e = final vs') \/
+  (exists (ei : expr) (vsi : value_stack),
+    eval_step vs e = middle ei vsi /\
+    Sem_expr vsi ei vs').
+Proof.
+  intros e vs vs' Hsem.
+  (* Proceed by induction on the semantics. *)
+  induction Hsem.
+  - inversion H; (* The expression is just an intrnsic. *)
+    (* Dismiss all the straightforward "final" cases,
+       of which most intrinsics are. *)
+    try (left; reflexivity).
+    (* Only apply remains; We are in an intermediate / middle case. *)
+    right.
+    (* The semantics guarantee that the expression in the
+       quote evaluates to the final state. *)
+    exists e, vs0. auto.
+  - (* The expression is a quote. This is yet another final case. *)
+    left; reflexivity.
+  - (* The composition is never a final step, since we have to evaluate both
+       branches to "finish up". *)
+    destruct IHHsem1; right.
+    + (* If the left branch finihed, only the right branch needs to be evaluted. *)
+      simpl. rewrite H. exists e2, vs2. auto.
+    + (* Otherwise, the left branch has an intermediate evaluation, guaranteed
+         by induction to be consitent. *)
+      destruct H as [ei [vsi [Heval Hsem']]].
+      (* We compose the remaining part of the left branch with the right branch. *)
+      exists (e_comp ei e2), vsi. simpl.
+      (* The evaluation is trivially to a "middle" state. *)
+      rewrite Heval. split. auto.
+      eapply Sem_e_comp. apply Hsem'. apply Hsem2.
+Qed.
+
+Inductive eval_chain (vs : value_stack) (e : expr) (vs' : value_stack) : Prop :=
+  | chain_final (P : eval_step vs e = final vs')
+  | chain_middle (ei : expr) (vsi : value_stack)
+      (P : eval_step vs e = middle ei vsi) (rest : eval_chain vsi ei vs').
+
+Lemma eval_chain_merge : forall (e1 e2 : expr) (vs vs' vs'' : value_stack),
+  eval_chain vs e1 vs' -> eval_chain vs' e2 vs'' -> eval_chain vs (e_comp e1 e2) vs''.
+Proof.
+  intros e1 e2 vs vs' vs'' ch1 ch2.
+  induction ch1;
+  eapply chain_middle; simpl; try (rewrite P); auto.
+Qed.
+
+Lemma eval_chain_split : forall (e1 e2 : expr) (vs vs'' : value_stack),
+  eval_chain vs (e_comp e1 e2) vs'' -> exists vs', (eval_chain vs e1 vs') /\ (eval_chain vs' e2 vs'').
+Proof.
+  intros e1 e2 vs vss'' ch.
+  ltac1:(dependent induction ch).
+  - simpl in P. destruct (eval_step vs e1); inversion P.
+  - simpl in P. destruct (eval_step vs e1) eqn:Hval; try (inversion P).
+    + injection P as Hinj; subst. specialize (IHch e e2 H0) as [s'0 [ch1 ch2]].
+      eexists. split.
+      * eapply chain_middle. apply Hval. apply ch1.
+      * apply ch2.
+    + subst. eexists. split.
+      * eapply chain_final. apply Hval.
+      * apply ch.
+Qed.
+
+Theorem val_step_sem : forall (e : expr) (vs vs' : value_stack),
+  Sem_expr vs e vs' -> eval_chain vs e vs'
+with eval_step_int : forall (i : intrinsic) (vs vs' : value_stack),
+  Sem_int vs i vs' -> eval_chain vs (e_int i) vs'.
+Proof.
+  - intros e vs vs' Hsem.
+    induction Hsem.
+    + (* This is an intrinsic, which is handled by the second
+         theorem, eval_step_int. This lemma is used here. *)
+      auto.
+    + (* A quote doesn't have a next step, and so is final. *)
+      apply chain_final. auto.
+    + (* In composition, by induction, we know that the two sub-expressions produce
+         proper evaluation chains. Chains can be composed (via eval_chain_merge). *)
+      eapply eval_chain_merge; eauto.
+  - intros i vs vs' Hsem.
+    (* The evaluation chain depends on the specific intrinsic in use. *)
+    inversion Hsem; subst;
+    (* Most intrinsics produce a final value, and the evaluation chain is trivial. *)
+    try (apply chain_final; auto; fail).
+    (* Only apply is non-final. The first step is popping the quote from the stack,
+       and the rest of the steps are given by the evaluation of the code in the quote. *)
+    apply chain_middle with e vs0; auto.
+Qed.
+
+Ltac2 Type exn ::= [ | Not_intrinsic ].
+
+Ltac2 rec destruct_n (n : int) (vs : constr) : unit :=
+  if Int.le n 0 then () else
+    let v := Fresh.in_goal @v in
+    let vs' := Fresh.in_goal @vs in
+    destruct $vs as [|$v $vs']; Control.enter (fun () =>
+      try (destruct_n (Int.sub n 1) (Control.hyp vs'))
+    ).
+
+Ltac2 int_arity (int : constr) : int :=
+  match! int with
+  | swap => 2
+  | clone => 1
+  | drop => 1
+  | quote => 1
+  | compose => 2
+  | apply => 1
+  | _ => Control.throw Not_intrinsic
+  end.
+
+Ltac2 destruct_int_stack (int : constr) (va: constr) := destruct_n (int_arity int) va.
+
+Ltac2 ensure_valid_stack () := Control.enter (fun () =>
+  match! goal with
+  | [h : eval_step ?a (e_int ?b) = ?c |- _] =>
+      let h := Control.hyp h in
+      destruct_int_stack b a;
+      try (inversion $h; fail)
+  | [|- _ ] => ()
+  end).
+
+Theorem test : forall (vs vs': value_stack), eval_step vs (e_int swap) = final vs' ->
+  exists v1 v2 vs'', vs = v1 :: v2 :: vs'' /\ vs' = v2 :: v1 :: vs''.
+Proof.
+  intros s s' Heq.
+  ensure_valid_stack ().
+  simpl in Heq. injection Heq as Hinj. subst. eauto.
+Qed.
+
+Theorem eval_step_final_sem : forall (e : expr) (vs vs' : value_stack),
+  eval_step vs e = final vs' -> Sem_expr vs e vs'.
+Proof.
+  intros e vs vs' Hev. destruct e.
+  - destruct i; ensure_valid_stack ();
+    (* Get rid of trivial cases that match one-to-one. *)
+    simpl in Hev; try (injection Hev as Hinj; subst; solve_basic ()).
+    + (* compose with one quoted value is not final, but an error. *)
+      destruct v. inversion Hev.
+    + (* compose with two quoted values. *)
+      destruct v; destruct v0.
+      injection Hev as Hinj; subst; solve_basic ().
+    + (* Apply is not final. *) destruct v. inversion Hev.
+  - (* Quote is always final, trivially, and the semantics match easily. *)
+    simpl in Hev. injection Hev as Hinj; subst. solve_basic ().
+  - (* Compose is never final, so we don't need to handle it here. *)
+    simpl in Hev. destruct (eval_step vs e1); inversion Hev.
+Qed.
+
+Theorem eval_step_middle_sem : forall (e ei: expr) (vs vsi vs' : value_stack),
+  eval_step vs e = middle ei vsi ->
+  Sem_expr vsi ei vs' ->
+  Sem_expr vs e vs'.
+Proof.
+  intros e. induction e; intros ei vs vsi vs' Hev Hsem.
+  - destruct i; ensure_valid_stack ().
+    + (* compose with one quoted value; invalid. *)
+      destruct v. inversion Hev.
+    + (* compose with two quoted values; not a middle step. *)
+      destruct v; destruct v0. inversion Hev.
+    + (* Apply *)
+      destruct v. injection Hev as Hinj; subst.
+      solve_basic (). auto.
+  - (* quoting an expression is not middle. *)
+    inversion Hev.
+  - simpl in Hev.
+    destruct (eval_step vs e1) eqn:Hev1.
+    + (* Step led to an error, which can't happen in a chain. *)
+      inversion Hev.
+    + (* Left expression makes a non-final step. Milk this for equalities first. *)
+      injection Hev as Hinj; subst.
+      (* The rest of the program (e_comp e e2) evaluates using our semantics,
+         which means that both e and e2 evaluate using our semantics. *)
+      inversion Hsem; subst.
+      (* By induction, e1 evaluates using our semantics if e does, which we just confirmed. *)
+      specialize (IHe1 e vs vsi vs2 Hev1 H2).
+      (* The composition rule can now be applied. *)
+      eapply Sem_e_comp; eauto.
+    + (* Left expression makes a final step. Milk this for equalities first. *)
+      injection Hev as Hinj; subst.
+      (* Using eval_step_final, we know that e1 evaluates to the intermediate
+         state given our semantics. *)
+      specialize (eval_step_final_sem e1 vs vsi Hev1) as Hsem1.
+      (* The composition rule can now be applied. *)
+      eapply Sem_e_comp; eauto.
+Qed.
+
+Theorem eval_step_sem_back : forall (e : expr) (vs vs' : value_stack),
+  eval_chain vs e vs' -> Sem_expr vs e vs'.
+Proof.
+  intros e vs vs' ch.
+  ltac1:(dependent induction ch).
+  - apply eval_step_final_sem. auto.
+  - specialize (eval_step_middle_sem e ei vs vsi vs' P IHch). auto.
+Qed.
+
+Corollary eval_step_no_sem : forall (e : expr) (vs vs' : value_stack),
+  ~(Sem_expr vs e vs') -> ~(eval_chain vs e vs').
+Proof.
+  intros e vs vs' Hnsem Hch.
+  specialize (eval_step_sem_back _ _ _ Hch). auto.
+Qed.
+
+Require Extraction.
+Require Import ExtrHaskellBasic.
+Extraction Language Haskell.
+Set Extraction KeepSingleton.
+Extraction "UccGen.hs" expr eval_step true false or.
+
+Remark eval_swap_two_values : forall (vs vs' : value_stack),
+  eval_step vs (e_int swap) = final vs' -> exists v1 v2 vst, vs = v1 :: v2 :: vst /\ vs' = v2 :: v1 :: vst.
+Proof.
+  intros vs vs' Hev.
+  (* Can't proceed until we know more about the stack. *)
+  destruct vs as [|v1 [|v2 vs]].
+  - (* Invalid case; empty stack. *) inversion Hev.
+  - (* Invalid case; stack only has one value. *) inversion Hev.
+  - (* Valid case: the stack has two values. *) injection Hev. eauto.
+Qed.
+
+Remark eval_swap_two_values' : forall (vs vs' : value_stack),
+  eval_step vs (e_int swap) = final vs' -> exists v1 v2 vst, vs = v1 :: v2 :: vst /\ vs' = v2 :: v1 :: vst.
+Proof.
+  intros vs vs' Hev.
+  ensure_valid_stack ().
+  injection Hev. eauto.
+Qed.
--- a/code/dawn/DawnV2.v
+++ b/code/dawn/DawnV2.v
@@ -0,0 +1,179 @@
+Require Import Coq.Lists.List.
+From Ltac2 Require Import Ltac2.
+
+Inductive intrinsic :=
+  | swap
+  | clone
+  | drop
+  | quote
+  | compose
+  | apply.
+
+Inductive expr :=
+  | e_int (i : intrinsic)
+  | e_quote (e : expr)
+  | e_comp (e1 e2 : expr).
+
+Definition e_compose (e : expr) (es : list expr) := fold_left e_comp es e.
+
+Inductive value := v_quote (e : expr).
+Definition value_stack := list value.
+
+Definition value_to_expr (v : value) : expr :=
+  match v with
+  | v_quote e => e_quote e
+  end.
+
+Inductive Sem_int : value_stack -> intrinsic -> value_stack -> Prop :=
+  | Sem_swap : forall (v v' : value) (vs : value_stack), Sem_int (v' :: v :: vs) swap (v :: v' :: vs)
+  | Sem_clone : forall (v : value) (vs : value_stack), Sem_int (v :: vs) clone (v :: v :: vs)
+  | Sem_drop : forall (v : value) (vs : value_stack), Sem_int (v :: vs) drop vs
+  | Sem_quote : forall (v : value) (vs : value_stack), Sem_int (v :: vs) quote ((v_quote (value_to_expr v)) :: vs)
+  | Sem_compose : forall (e e' : expr) (vs : value_stack), Sem_int (v_quote e' :: v_quote e :: vs) compose (v_quote (e_comp e e') :: vs)
+  | Sem_apply : forall (e : expr) (vs vs': value_stack), Sem_expr vs e vs' -> Sem_int (v_quote e :: vs) apply vs'
+
+with Sem_expr : value_stack -> expr -> value_stack -> Prop :=
+  | Sem_e_int : forall (i : intrinsic) (vs vs' : value_stack), Sem_int vs i vs' -> Sem_expr vs (e_int i) vs'
+  | Sem_e_quote : forall (e : expr) (vs : value_stack), Sem_expr vs (e_quote e) (v_quote e :: vs)
+  | Sem_e_comp : forall (e1 e2 : expr) (vs1 vs2 vs3 : value_stack),
+      Sem_expr vs1 e1 vs2 -> Sem_expr vs2 e2 vs3 -> Sem_expr vs1 (e_comp e1 e2) vs3.
+
+Definition false : expr := e_quote (e_int drop).
+Definition false_v : value := v_quote (e_int drop).
+
+Definition true : expr := e_quote (e_comp (e_int swap) (e_int drop)).
+Definition true_v : value := v_quote (e_comp (e_int swap) (e_int drop)).
+
+Theorem false_correct : forall (v v' : value) (vs : value_stack), Sem_expr (v' :: v :: vs) (e_comp false (e_int apply)) (v :: vs).
+Proof.
+  intros v v' vs.
+  eapply Sem_e_comp.
+  - apply Sem_e_quote.
+  - apply Sem_e_int. apply Sem_apply. apply Sem_e_int. apply Sem_drop.
+Qed.
+
+Theorem true_correct : forall (v v' : value) (vs : value_stack), Sem_expr (v' :: v :: vs) (e_comp true (e_int apply)) (v' :: vs).
+Proof.
+  intros v v' vs.
+  eapply Sem_e_comp.
+  - apply Sem_e_quote.
+  - apply Sem_e_int. apply Sem_apply. eapply Sem_e_comp.
+    * apply Sem_e_int. apply Sem_swap.
+    * apply Sem_e_int. apply Sem_drop.
+Qed.
+
+Definition or : expr := e_comp (e_int clone) (e_int apply).
+
+Theorem or_false_v : forall (v : value) (vs : value_stack), Sem_expr (false_v :: v :: vs) or (v :: vs).
+Proof with apply Sem_e_int.
+  intros v vs.
+  eapply Sem_e_comp...
+  - apply Sem_clone.
+  - apply Sem_apply... apply Sem_drop.
+Qed.
+
+Theorem or_true : forall (v : value) (vs : value_stack), Sem_expr (true_v :: v :: vs) or (true_v :: vs).
+Proof with apply Sem_e_int.
+  intros v vs.
+  eapply Sem_e_comp...
+  - apply Sem_clone...
+  - apply Sem_apply. eapply Sem_e_comp...
+    * apply Sem_swap.
+    * apply Sem_drop.
+Qed.
+
+Definition or_false_false := or_false_v false_v.
+Definition or_false_true := or_false_v true_v.
+Definition or_true_false := or_true false_v.
+Definition or_true_true := or_true true_v.
+
+Fixpoint quote_n (n : nat) :=
+  match n with
+  | O => e_int quote
+  | S n' => e_compose (quote_n n') (e_int swap :: e_int quote :: e_int swap :: e_int compose :: nil)
+  end.
+
+Theorem quote_2_correct : forall (v1 v2 : value) (vs : value_stack),
+    Sem_expr (v2 :: v1 :: vs) (quote_n 1) (v_quote (e_comp (value_to_expr v1) (value_to_expr v2)) :: vs).
+Proof with apply Sem_e_int.
+  intros v1 v2 vs. simpl.
+  repeat (eapply Sem_e_comp)...
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_compose.
+Qed.
+
+Theorem quote_3_correct : forall (v1 v2 v3 : value) (vs : value_stack),
+  Sem_expr (v3 :: v2 :: v1 :: vs) (quote_n 2) (v_quote (e_comp (value_to_expr v1) (e_comp (value_to_expr v2) (value_to_expr v3))) :: vs).
+Proof with apply Sem_e_int.
+  intros v1 v2 v3 vs. simpl.
+  repeat (eapply Sem_e_comp)...
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_compose.
+  - apply Sem_swap.
+  - apply Sem_quote.
+  - apply Sem_swap.
+  - apply Sem_compose.
+Qed.
+
+Ltac2 rec solve_basic () := Control.enter (fun _ =>
+  match! goal with
+  | [|- Sem_int ?vs1 swap ?vs2] => apply Sem_swap
+  | [|- Sem_int ?vs1 clone ?vs2] => apply Sem_clone
+  | [|- Sem_int ?vs1 drop ?vs2] => apply Sem_drop
+  | [|- Sem_int ?vs1 quote ?vs2] => apply Sem_quote
+  | [|- Sem_int ?vs1 compose ?vs2] => apply Sem_compose
+  | [|- Sem_int ?vs1 apply ?vs2] => apply Sem_apply
+  | [|- Sem_expr ?vs1 (e_comp ?e1 ?e2) ?vs2] => eapply Sem_e_comp; solve_basic ()
+  | [|- Sem_expr ?vs1 (e_int ?e) ?vs2] => apply Sem_e_int; solve_basic ()
+  | [|- Sem_expr ?vs1 (e_quote ?e) ?vs2] => apply Sem_e_quote
+  | [_ : _ |- _] => ()
+  end).
+
+Theorem quote_2_correct' : forall (v1 v2 : value) (vs : value_stack),
+    Sem_expr (v2 :: v1 :: vs) (quote_n 1) (v_quote (e_comp (value_to_expr v1) (value_to_expr v2)) :: vs).
+Proof. intros. simpl. solve_basic (). Qed.
+
+Theorem quote_3_correct' : forall (v1 v2 v3 : value) (vs : value_stack),
+  Sem_expr (v3 :: v2 :: v1 :: vs) (quote_n 2) (v_quote (e_comp (value_to_expr v1) (e_comp (value_to_expr v2) (value_to_expr v3))) :: vs).
+Proof. intros. simpl. solve_basic (). Qed.
+
+Definition rotate_n (n : nat) := e_compose (quote_n n) (e_int swap :: e_int quote :: e_int compose :: e_int apply :: nil).
+
+Lemma eval_value : forall (v : value) (vs : value_stack),
+  Sem_expr vs (value_to_expr v) (v :: vs).
+Proof.
+  intros v vs.
+  destruct v. 
+  simpl. apply Sem_e_quote.
+Qed.
+
+Theorem rotate_3_correct : forall (v1 v2 v3 : value) (vs : value_stack),
+  Sem_expr (v3 :: v2 :: v1 :: vs) (rotate_n 1) (v1 :: v3 :: v2 :: vs).
+Proof.
+  intros. unfold rotate_n. simpl. solve_basic ().
+  repeat (eapply Sem_e_comp); apply eval_value.
+Qed.
+
+Theorem rotate_4_correct : forall (v1 v2 v3 v4 : value) (vs : value_stack),
+  Sem_expr (v4 :: v3 :: v2 :: v1 :: vs) (rotate_n 2) (v1 :: v4 :: v3 :: v2 :: vs).
+Proof.
+  intros. unfold rotate_n. simpl. solve_basic ().
+  repeat (eapply Sem_e_comp); apply eval_value.
+Qed.
+
+Theorem e_comp_assoc : forall (e1 e2 e3 : expr) (vs vs' : value_stack),
+  Sem_expr vs (e_comp e1 (e_comp e2 e3)) vs' <-> Sem_expr vs (e_comp (e_comp e1 e2) e3) vs'.
+Proof.
+  intros e1 e2 e3 vs vs'.
+  split; intros Heval.
+  - inversion Heval; subst. inversion H4; subst.
+    eapply Sem_e_comp. eapply Sem_e_comp. apply H2. apply H3. apply H6.
+  - inversion Heval; subst. inversion H2; subst.
+    eapply Sem_e_comp. apply H3. eapply Sem_e_comp. apply H6. apply H4.
+Qed.
--- a/code/dawn/Ucc.hs
+++ b/code/dawn/Ucc.hs
@@ -0,0 +1,64 @@
+module Ucc where
+import UccGen
+import Text.Parsec
+import Data.Functor.Identity
+import Control.Applicative hiding ((<|>))
+import System.IO
+
+instance Show Intrinsic where
+    show Swap = "swap"
+    show Clone = "clone"
+    show Drop = "drop"
+    show Quote = "quote"
+    show Compose = "compose"
+    show Apply = "apply"
+
+instance Show Expr where
+    show (E_int i) = show i
+    show (E_quote e) = "[" ++ show e ++ "]"
+    show (E_comp e1 e2) = show e1 ++ " " ++ show e2
+
+instance Show Value where
+    show (V_quote e) = show (E_quote e)
+
+type Parser a = ParsecT String () Identity a
+
+intrinsic :: Parser Intrinsic
+intrinsic = (<* spaces) $ foldl1 (<|>) $ map (\(s, i) -> try (string s >> return i))
+    [ ("swap", Swap)
+    , ("clone", Clone)
+    , ("drop", Drop)
+    , ("quote", Quote)
+    , ("compose", Compose)
+    , ("apply", Apply)
+    ]
+
+expression :: Parser Expr
+expression = foldl1 E_comp <$> many1 single
+    where
+        single
+            = (E_int <$> intrinsic)
+            <|> (fmap E_quote $ char '[' *> spaces *> expression <* char ']' <* spaces)
+
+parseExpression :: String -> Either ParseError Expr
+parseExpression = runParser expression () "<inline>"
+
+eval :: [Value] -> Expr -> Maybe [Value]
+eval s e =
+    case eval_step s e of
+        Err -> Nothing
+        Final s' -> Just s'
+        Middle e' s' -> eval s' e'
+
+main :: IO ()
+main = do
+    putStr "> "
+    hFlush stdout
+    str <- getLine
+    case parseExpression str of
+        Right e ->
+            case eval [] e of
+                Just st -> putStrLn $ show st
+                _ -> putStrLn "Evaluation error"
+        _ -> putStrLn "Parse error"
+    main
--- a/code/typescript-emitter/js1.js
+++ b/code/typescript-emitter/js1.js
@@ -0,0 +1,23 @@
+class EventEmitter {
+    constructor() {
+        this.handlers = {}
+    }
+
+    emit(event) {
+        this.handlers[event]?.forEach(h => h());
+    }
+
+    addHandler(event, handler) {
+        if(!this.handlers[event]) {
+            this.handlers[event] = [handler];
+        } else {
+            this.handlers[event].push(handler);
+        }
+    }
+}
+
+const emitter = new EventEmitter();
+emitter.addHandler("start", () => console.log("Started!"));
+emitter.addHandler("end", () => console.log("Ended!"));
+emitter.emit("end");
+emitter.emit("start");
--- a/code/typescript-emitter/js2.js
+++ b/code/typescript-emitter/js2.js
@@ -0,0 +1,23 @@
+class EventEmitter {
+    constructor() {
+        this.handlers = {}
+    }
+
+    emit(event, value) {
+        this.handlers[event]?.forEach(h => h(value));
+    }
+
+    addHandler(event, handler) {
+        if(!this.handlers[event]) {
+            this.handlers[event] = [handler];
+        } else {
+            this.handlers[event].push(handler);
+        }
+    }
+}
+
+const emitter = new EventEmitter();
+emitter.addHandler("numberChange", n => console.log("New number value is: ", n));
+emitter.addHandler("stringChange", s => console.log("New string value is: ", s));
+emitter.emit("numberChange", 1);
+emitter.emit("stringChange", "3");
--- a/code/typescript-emitter/ts.ts
+++ b/code/typescript-emitter/ts.ts
@@ -0,0 +1,27 @@
+class EventEmitter<T> {
+    private handlers: { [eventName in keyof T]?: ((value: T[eventName]) => void)[] }
+
+    constructor() {
+        this.handlers = {}
+    }
+
+    emit<K extends keyof T>(event: K, value: T[K]): void {
+        this.handlers[event]?.forEach(h => h(value));
+    }
+
+    addHandler<K extends keyof T>(event: K, handler: (value: T[K]) => void): void {
+        if(!this.handlers[event]) {
+            this.handlers[event] = [handler];
+        } else {
+            this.handlers[event].push(handler);
+        }
+    }
+}
+
+const emitter = new EventEmitter<{ numberChange: number, stringChange: string }>();
+emitter.addHandler("numberChange", n => console.log("New number value is: ", n));
+emitter.addHandler("stringChange", s => console.log("New string value is: ", s));
+emitter.emit("numberChange", 1);
+emitter.emit("stringChange", "3");
+emitter.emit("numberChange", "1");
+emitter.emit("stringChange", 3);
--- a/content/blog/00_cs325_languages_hw1.md
+++ b/content/blog/00_cs325_languages_hw1.md
@@ -1,7 +1,7 @@
 ---
 title: A Language for an Assignment - Homework 1
 date: 2019-12-27T23:27:09-08:00
-tags: ["Haskell", "Python", "Algorithms"]
+tags: ["Haskell", "Python", "Algorithms", "Programming Languages"]
 ---

 On a rainy Oregon day, I was walking between classes with a group of friends.
--- a/content/blog/01_cs325_languages_hw2.md
+++ b/content/blog/01_cs325_languages_hw2.md
@@ -1,7 +1,7 @@
 ---
 title: A Language for an Assignment - Homework 2
 date: 2019-12-30T20:05:10-08:00
-tags: ["Haskell", "Python", "Algorithms"]
+tags: ["Haskell", "Python", "Algorithms", "Programming Languages"]
 ---

 After the madness of the
--- a/content/blog/02_cs325_languages_hw3.md
+++ b/content/blog/02_cs325_languages_hw3.md
@@ -1,7 +1,7 @@
 ---
 title: A Language for an Assignment - Homework 3
 date: 2020-01-02T22:17:43-08:00
-tags: ["Haskell", "Python", "Algorithms"]
+tags: ["Haskell", "Python", "Algorithms", "Programming Languages"]
 ---

 It rained in Sunriver on New Year's Eve, and it continued to rain
--- a/content/blog/coq_dawn.md
+++ b/content/blog/coq_dawn.md
@@ -0,0 +1,377 @@
+---
+title: "Formalizing Dawn in Coq"
+date: 2021-11-20T19:04:57-08:00
+tags: ["Coq", "Dawn", "Programming Languages"]
+description: "In this article, we use Coq to write down machine-checked semantics for the untyped concatenative calculus."
+---
+
+The [_Foundations of Dawn_](https://www.dawn-lang.org/posts/foundations-ucc/) article came up
+on [Lobsters](https://lobste.rs/s/clatuv/foundations_dawn_untyped_concatenative) recently.
+In this article, the author of Dawn defines a core calculus for the language, and provides its
+semantics. The core calculus is called the _untyped concatenative calculus_, or UCC.
+The definitions in the semantics seemed so clean and straightforward that I wanted to try my hand at
+translating them into machine-checked code. I am most familiar with [Coq](https://coq.inria.fr/),
+and that's what I reached for when making this attempt.
+
+### Defining the Syntax
+#### Expressions and Intrinsics
+This is mostly the easy part. A UCC expression is one of three things:
+
+* An "intrinsic", written \\(i\\), which is akin to a built-in function or command.
+* A "quote", written \\([e]\\), which takes a UCC expression \\(e\\) and moves it onto the stack (UCC is stack-based).
+* A composition of several expressions, written \\(e_1\\ e_2\\ \\ldots\\ e_n\\), which effectively evaluates them in order.
+
+This is straightforward to define in Coq, but I'm going to make a little simplifying change.
+Instead of making "composition of \\(n\\) expressions" a core language feature, I'll only
+allow "composition of \\(e_1\\) and \\(e_2\\)", written \\(e_1\\ e_2\\). This change does not
+in any way reduce the power of the language; we can still
+{{< sidenote "right" "assoc-note" "write \(e_1\ e_2\ \ldots\ e_n\) as \((e_1\ e_2)\ \ldots\ e_n\)." >}}
+The same expression can, of course, be written as \(e_1\ \ldots\ (e_{n-1}\ e_n)\).
+So, which way should we <em>really</em> use when translating the many-expression composition
+from the Dawn article into the two-expression composition I am using here? Well, the answer is,
+it doesn't matter; expression composition is <em>associative</em>, so both ways effectively mean
+the same thing.<br>
+<br>
+This is quite similar to what we do in algebra: the regular old addition operator, \(+\) is formally
+only defined for pairs of numbers, like \(a+b\). However, no one really bats an eye when we
+write \(1+2+3\), because we can just insert parentheses any way we like, and get the same result:
+\((1+2)+3\) is the same as \(1+(2+3)\).
+{{< /sidenote >}}
+With that in mind, we can translate each of the three types of expressions in UCC into cases
+of an inductive data type in Coq.
+
+{{< codelines "Coq" "dawn/Dawn.v" 12 15 >}}
+
+Why do we need `e_int`? We do because a token like \\(\\text{swap}\\) can be viewed
+as belonging to the set of intrinsics \\(i\\), or the set of expressions, \\(e\\). While writing
+down the rules in mathematical notation, what exactly the token means is inferred from context - clearly
+\\(\\text{swap}\\ \\text{drop}\\) is an expression built from two other expressions. In statically-typed
+functional languages like Coq or Haskell, however, the same expression can't belong to two different,
+arbitrary types. Thus, to turn an intrinsic into an expression, we need to wrap it up in a constructor,
+which we called `e_int` here. Other than that, `e_quote` accepts as argument another expression, `e` (the
+thing being quoted), and `e_comp` accepts two expressions, `e1` and `e2` (the two sub-expressions being composed).
+
+The definition for intrinsics themselves is even simpler:
+
+{{< codelines "Coq" "dawn/Dawn.v" 4 10 >}}
+
+We simply define a constructor for each of the six intrinsics. Since none of the intrinsic
+names are reserved in Coq, we can just call our constructors exactly the same as their names
+in the written formalization.
+
+#### Values and Value Stacks
+Values are up next. My initial thought was to define a value much like
+I defined an intrinsic expression: by wrapping an expression in a constructor for a new data
+type. Something like:
+
+```Coq
+Inductive value :=
+    | v_quot (e : expr).
+```
+
+Then, `v_quot (e_int swap)` would be the Coq translation of the expression \\([\\text{swap}]\\). 
+However, I didn't decide on this approach for two reasons:
+
+* There are now two ways to write a quoted expression: either `v_quote e` to represent
+  a quoted expression that is a value, or `e_quote e` to represent a quoted expression
+  that is just an expression. In the extreme case, the value \\([[e]]\\) would
+  be represented by `v_quote (e_quote e)` - two different constructors for the same concept,
+  in the same expression!
+* When formalizing the lambda calculus,
+  [Programming Language Foundations](https://softwarefoundations.cis.upenn.edu/plf-current/Stlc.html)
+  uses an inductively-defined property to indicate values. In the simply typed lambda calculus,
+  much like in UCC, values are a subset of expressions.
+
+I took instead the approach from Programming Language Foundations: a value is merely an expression
+for which some predicate, `IsValue`, holds. We will define this such that `IsValue (e_quote e)` is provable,
+but also such that here is no way to prove `IsValue (e_int swap)`, since _that_ expression is not
+a value. But what does "provable" mean, here?
+
+By the [Curry-Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence),
+a predicate is just a function that takes _something_ and returns a type. Thus, if \\(\\text{Even}\\)
+is a predicate, then \\(\\text{Even}\\ 3\\) is actually a type. Since \\(\\text{Even}\\) takes
+numbers in, it is a predicate on numbers. Our \\(\\text{IsValue}\\) predicate will be a predicate
+on expressions, instead. In Coq, we can write this as:
+
+{{< codelines "Coq" "dawn/Dawn.v" 19 19 >}}
+
+You might be thinking,
+
+> Huh, `Prop`? But you just said that predicates return types!
+
+This is a good observation; In Coq, `Prop` is a special sort of type that corresponds to logical
+propositions. It's special for a few reasons, but those reasons are beyond the scope of this post;
+for our purposes, it's sufficient to think of `IsValue e` as a type.
+
+Alright, so what good is this new `IsValue e` type? Well, we will define `IsValue` such that
+this type is only _inhabited_ if `e` is a value according to the UCC specification. A type
+is inhabited if and only if we can find a value of that type. For instance, the type of natural
+numbers, `nat`, is inhabited, because any number, like `0`, has this type. Uninhabited types
+are harder to come by, but take as an example the type `3 = 4`, the type of proofs that three is equal
+to four. Three is _not_ equal to four, so we can never find a proof of equality, and thus, `3 = 4` is
+uninhabited. As I said, `IsValue e` will only be inhabited if `e` is a value per the formal
+specification of UCC; specifically, this means that `e` is a quoted expression, like `e_quote e'`.
+
+To this end, we define `IsValue` as follows:
+
+{{< codelines "Coq" "dawn/Dawn.v" 19 20 >}}
+
+Now, `IsValue` is a new data type with only only constructor, `ValQuote`. For any expression `e`,
+this constructor creates a value of type `IsValue (e_quote e)`. Two things are true here:
+
+* Since `Val_quote` accepts any expression `e` to be put inside `e_quote`, we can use
+  `Val_quote` to create an `IsValue` instance for any quoted expression.
+* Because `Val_quote` is the _only_ constructor, and because it always returns `IsValue (e_quote e)`,
+  there's no way to get `IsValue (e_int i)`, or anything else.
+
+Thus, `IsValue e` is inhabited if and only if `e` is a UCC value, as we intended.
+
+Just one more thing. A value is just an expression, but Coq only knows about this as long
+as there's an `IsValue` instance around to vouch for it. To be able to reason about values, then,
+we will need both the expression and its `IsValue` proof. Thus, we define the type `value` to mean
+a pair of two things: an expression `v` and a proof that it's a value, `IsValue v`:
+
+{{< codelines "Coq" "dawn/Dawn.v" 22 22 >}}
+
+A value stack is just a list of values:
+
+{{< codelines "Coq" "dawn/Dawn.v" 23 23 >}}
+
+### Semantics
+Remember our `IsValue` predicate? Well, it's not just any predicate, it's a _unary_ predicate.
+_Unary_ means that it's a predicate that only takes one argument, an expression in our case. However,
+this is far from the only type of predicate. Here are some examples:
+
+* Equality, `=`, is a binary predicate in Coq. It takes two arguments, say `x` and `y`, and builds
+  a type `x = y` that is only inhabited if `x` and `y` are equal.
+* The mathematical "less than" relation is also a binary predicate, and it's called `le` in Coq.
+  It takes two numbers `n` and `m` and returns a type `le n m` that is only inhabited if `n` is less
+  than or equal to `m`.
+* The evaluation relation in UCC is a ternary predicate. It takes two stacks, `vs` and `vs'`,
+  and an expression, `e`, and creates a type that's inhabited if and only if evaluating
+  `e` starting at a stack `vs` results in the stack `vs'`.
+
+Binary predicates are just functions of two inputs that return types. For instance, here's what Coq has
+to say about the type of `eq`:
+
+```
+eq : ?A -> ?A -> Prop
+```
+
+By a similar logic, ternary predicates, much like UCC's evaluation relation, are functions
+of three inputs. We can thus write the type of our evaluation relation as follows:
+
+{{< codelines "Coq" "dawn/Dawn.v" 35 35 >}}
+
+We define the constructors just like we did in our `IsValue` predicate. For each evaluation
+rule in UCC, such as:
+
+{{< latex >}}
+\langle V, v, v'\rangle\ \text{swap}\ \rightarrow\ \langle V, v', v \rangle
+{{< /latex >}}
+
+We introduce a constructor. For the `swap` rule mentioned above, the constructor looks like this:
+
+{{< codelines "Coq" "dawn/Dawn.v" 28 28 >}}
+
+Although the stacks are written in reverse order (which is just a consequence of Coq's list notation),
+I hope that the correspondence is fairly clear. If it's not, try reading this rule out loud:
+
+> The rule `Sem_swap` says that for every two values `v` and `v'`, and for any stack `vs`,
+  evaluating `swap` in the original stack `v' :: v :: vs`, aka \\(\\langle V, v, v'\\rangle\\),
+  results in a final stack `v :: v' :: vs`, aka \\(\\langle V, v', v\\rangle\\).
+
+With that in mind, here's a definition of a predicate `Sem_int`, the evaluation predicate
+for intrinsics:
+
+{{< codelines "Coq" "dawn/Dawn.v" 27 33 >}}
+
+Hey, what's all this with `v_quote` and `projT1`? It's just a little bit of bookkeeping.
+Given a value -- a pair of an expression `e` and a proof `IsValue e` -- the function `projT1`
+just returns the expression `e`. That is, it's basically a way of converting a value back into
+an expression. The function `v_quote` takes us in the other direction: given an expression \\(e\\),
+it constructs a quoted expression \\([e]\\), and combines it with a proof that the newly constructed
+quote is a value.
+
+The above two function in combination help us define the `quote` intrinsic, which
+wraps a value on the stack in an additional layer of quotes. When we create a new quote, we
+need to push it onto the value stack, so it needs to be a value; we thus use `v_quote`. However,
+`v_quote` needs an expression to wrap in a quote, so we use `projT1` to extract the expression from
+the value on top of the stack.
+
+In addition to intrinsics, we also define the evaluation relation for actual expressions.
+
+{{< codelines "Coq" "dawn/Dawn.v" 35 39 >}}
+
+Here, we may as well go through the three constructors to explain what they mean:
+
+* `Sem_e_int` says that if the expression being evaluated is an intrinsic, and if the
+   intrinsic has an effect on the stack as described by `Sem_int` above, then the effect
+   of the expression itself is the same.
+* `Sem_e_quote` says that if the expression is a quote, then a corresponding quoted
+   value is placed on top of the stack.
+* `Sem_e_comp` says that if one expression `e1` changes the stack from `vs1` to `vs2`,
+   and if another expression `e2` takes this new stack `vs2` and changes it into `vs3`,
+   then running the two expressions one after another (i.e. composing them) means starting
+   at stack `vs1` and ending in stack `vs3`.
+
+### \\(\\text{true}\\), \\(\\text{false}\\), \\(\\text{or}\\) and Proofs
+Now it's time for some fun! The UCC language specification starts by defining two values:
+true and false. Why don't we do the same thing?
+
+|UCC Spec| Coq encoding |
+|---|----|
+|\\(\\text{false}\\)=\\([\\text{drop}]\\)| {{< codelines "Coq" "dawn/Dawn.v" 41 42 >}}
+|\\(\\text{true}\\)=\\([\\text{swap} \\ \\text{drop}]\\)| {{< codelines "Coq" "dawn/Dawn.v" 44 45 >}}
+
+Let's try prove that these two work as intended.
+
+{{< codelines "Coq" "dawn/Dawn.v" 47 53 >}}
+
+This is the first real proof in this article. Rather than getting into the technical details,
+I invite you to take a look at the "shape" of the proof:
+
+* After the initial use of `intros`, which brings the variables `v`, `v`, and `vs` into
+  scope, we start by applying `Sem_e_comp`. Intuitively, this makes sense - at the top level,
+  our expression, \\(\\text{false}\\ \\text{apply}\\),
+  is a composition of two other expressions, \\(\\text{false}\\) and \\(\\text{apply}\\).
+  Because of this, we need to use the rule from our semantics that corresponds to composition.
+* The composition rule requires that we describe the individual effects on the stack of the
+  two constituent expressions (recall that the first expression takes us from the initial stack `v1`
+  to some intermediate stack `v2`, and the second expression takes us from that stack `v2` to the
+  final stack `v3`). Thus, we have two "bullet points":
+  * The first expression, \\(\\text{false}\\), is just a quoted expression. Thus, the rule
+    `Sem_e_quote` applies, and the contents of the quote are puhsed onto the stack.
+  * The second expression, \\(\\text{apply}\\), is an intrinsic, so we need to use the rule
+    `Sem_e_int`, which handles the intrinsic case. This, in turn, requires that we show
+    the effect of the intrinsic itself; the `apply` intrinsic evaluates the quoted expression
+    on the stack.
+    The quoted expression contains the body of false, or \\(\\text{drop}\\). This is
+    once again an intrinsic, so we use `Sem_e_int`; the intrinsic in question is \\(\\text{drop}\\),
+    so the `Sem_drop` rule takes care of that.
+
+Following these steps, we arrive at the fact that evaluating `false` on the stack simply drops the top
+element, as specified. The proof for \\(\\text{true}\\) is very similar in spirit:
+
+{{< codelines "Coq" "dawn/Dawn.v" 55 63 >}}
+
+We can also formalize the \\(\\text{or}\\) operator:
+
+|UCC Spec| Coq encoding |
+|---|----|
+|\\(\\text{or}\\)=\\(\\text{clone}\\ \\text{apply}\\)| {{< codelines "Coq" "dawn/Dawn.v" 65 65 >}}
+
+We can write two top-level proofs about how this works: the first says that \\(\\text{or}\\),
+when the first argument is \\(\\text{false}\\), just returns the second argument (this is in agreement
+with the truth table, since \\(\\text{false}\\) is the identity element of \\(\\text{or}\\)).
+The proof proceeds much like before:
+
+{{< codelines "Coq" "dawn/Dawn.v" 67 73 >}}
+
+To shorten the proof a little bit, I used the `Proof with` construct from Coq, which runs
+an additional _tactic_ (like `apply`) whenever `...` is used.
+Because of this, in this proof writing `apply Sem_apply...` is the same
+as `apply Sem_apply. apply Sem_e_int`. Since the `Sem_e_int` rule is used a lot, this makes for a
+very convenient shorthand.
+
+Similarly, we prove that \\(\\text{or}\\) applied to \\(\\text{true}\\) always returns \\(\\text{true}\\).
+
+{{< codelines "Coq" "dawn/Dawn.v" 75 83 >}}
+
+Finally, the specific facts (like \\(\\text{false}\\ \\text{or}\\ \\text{false}\\) evaluating to \\(\\text{false}\\))
+can be expressed using our two new proofs, `or_false_v` and `or_true`.
+
+{{< codelines "Coq" "dawn/Dawn.v" 85 88 >}}
+
+### Derived Expressions
+#### Quotes
+The UCC specification defines \\(\\text{quote}_n\\) to make it more convenient to quote
+multiple terms. For example, \\(\\text{quote}_2\\) composes and quotes the first two values
+on the stack. This is defined in terms of other UCC expressions as follows:
+
+{{< latex >}}
+\text{quote}_n = \text{quote}_{n-1}\ \text{swap}\ \text{quote}\ \text{swap}\ \text{compose}
+{{< /latex >}}
+
+We can write this in Coq as follows:
+
+{{< codelines "Coq" "dawn/Dawn.v" 90 94 >}}
+
+This definition diverges slightly from the one given in the UCC specification; particularly,
+UCC's spec mentions that \\(\\text{quote}_n\\) is only defined for \\(n \\geq 1\\).However,
+this means that in our code, we'd have to somehow handle the error that would arise if the
+term \\(\\text{quote}\_0\\) is used. Instead, I defined `quote_n n` to simply mean
+\\(\\text{quote}\_{n+1}\\); thus, in Coq, no matter what `n` we use, we will have a valid
+expression, since `quote_n 0` will simply correspond to \\(\\text{quote}_1 = \\text{quote}\\).
+
+We can now attempt to prove that this definition is correct by ensuring that the examples given
+in the specification are valid. We may thus write,
+
+{{< codelines "Coq" "dawn/Dawn.v" 96 106 >}}
+
+We used a new tactic here, `repeat`, but overall, the structure of the proof is pretty straightforward:
+the definition of `quote_n` consists of many intrinsics, and we apply the corresponding rules
+one-by-one until we arrive at the final stack. Writing this proof was kind of boring, since
+I just had to see which intrinsic is being used in each step, and then write a line of `apply`
+code to handle that intrinsic. This gets worse for \\(\\text{quote}_3\\):
+
+{{< codelines "Coq" "dawn/Dawn.v" 108 122 >}}
+
+It's so long! Instead, I decided to try out Coq's `Ltac2` mechanism to teach Coq how
+to write proofs like this itself. Here's what I came up with:
+
+{{< codelines "Coq" "dawn/Dawn.v" 124 136 >}}
+
+You don't have to understand the details, but in brief, this checks what kind of proof
+we're asking Coq to do (for instance, if we're trying to prove that a \\(\\text{swap}\\)
+instruction has a particular effect), and tries to apply a corresponding semantic rule.
+Thus, it will try `Sem_swap` if the expression is \\(\\text{swap}\\), 
+`Sem_clone` if the expression is \\(\\text{clone}\\), and so on. Then, the two proofs become:
+
+{{< codelines "Coq" "dawn/Dawn.v" 138 144 >}}
+
+#### Rotations
+There's a little trick to formalizing rotations. Values have an important property:
+when a value is run against a stack, all it does is place itself on a stack. We can state
+this as follows:
+
+{{< latex >}}
+\langle V \rangle\ v = \langle V\ v \rangle
+{{< /latex >}}
+
+Or, in Coq,
+
+{{< codelines "Coq" "dawn/Dawn.v" 148 149 >}}
+
+This is the trick to how \\(\\text{rotate}_n\\) works: it creates a quote of \\(n\\) reordered and composed
+values on the stack, and then evaluates that quote. Since evaluating each value
+just places it on the stack, these values end up back on the stack, in the same order that they
+were in the quote. When writing the proof, `solve_basic ()` gets us almost all the way to the
+end (evaluating a list of values against a stack). Then, we simply apply the composition
+rule over and over, following it up with `eval_value` to prove that the each value is just being
+placed back on the stack.
+
+{{< codelines "Coq" "dawn/Dawn.v" 156 168 >}}
+
+### `e_comp` is Associative
+When composing three expressions, which way of inserting parentheses is correct?
+Is it \\((e_1\\ e_2)\\ e_3\\)? Or is it \\(e_1\\ (e_2\\ e_3)\\)? Well, both!
+Expression composition is associative, which means that the order of the parentheses
+doesn't matter. We state this in the following theorem, which says that the two
+ways of writing the composition, if they evaluate to anything, evaluate to the same thing.
+
+{{< codelines "Coq" "dawn/Dawn.v" 170 171 >}}
+
+### Conclusion
+That's all I've got in me for today. However, we got pretty far! The UCC specification
+says:
+
+> One of my long term goals for UCC is to democratize formal software verification in order to make it much more feasible and realistic to write perfect software.
+
+I think that UCC is definitely getting there: formally defining the semantics outlined
+on the page was quite straightforward. We can now have complete confidence in the behavior
+of \\(\\text{true}\\), \\(\\text{false}\\), \\(\\text{or}\\), \\(\\text{quote}_n\\) and
+\\(\\text{rotate}_n\\). The proof of associativity is also enough to possibly argue for simplifying
+the core calculus' syntax even more. All of this we got from an official source, with only
+a little bit of tweaking to get from the written description of the language to code! I'm
+looking forward to reading the next post about the _multistack_ concatenative calculus.
--- a/content/blog/coq_dawn_eval/coq_eval_chain_base.png
+++ b/content/blog/coq_dawn_eval/coq_eval_chain_base.png
--- a/content/blog/coq_dawn_eval/coq_eval_chain_inductive.png
+++ b/content/blog/coq_dawn_eval/coq_eval_chain_inductive.png
--- a/content/blog/coq_dawn_eval/coq_eval_chain_merge.png
+++ b/content/blog/coq_dawn_eval/coq_eval_chain_merge.png
--- a/content/blog/coq_dawn_eval/coq_eval_empty.png
+++ b/content/blog/coq_dawn_eval/coq_eval_empty.png
--- a/content/blog/coq_dawn_eval/coq_eval_lists.png
+++ b/content/blog/coq_dawn_eval/coq_eval_lists.png
--- a/content/blog/coq_dawn_eval/coq_eval_one.png
+++ b/content/blog/coq_dawn_eval/coq_eval_one.png
--- a/content/blog/coq_dawn_eval/coq_eval_two.png
+++ b/content/blog/coq_dawn_eval/coq_eval_two.png
--- a/content/blog/coq_dawn_eval/index.md
+++ b/content/blog/coq_dawn_eval/index.md
@@ -0,0 +1,638 @@
+---
+title: "A Verified Evaluator for the Untyped Concatenative Calculus"
+date: 2021-11-27T20:24:57-08:00
+tags: ["Dawn", "Coq", "Programming Languages"]
+---
+
+Earlier, I wrote [an article]({{< relref "./coq_dawn" >}}) in which I used Coq to
+encode the formal semantics of [Dawn's Untyped Concatenative Calculus](https://www.dawn-lang.org/posts/foundations-ucc/),
+and to prove a few things about the mini-language. Though I'm quite happy with how that turned out,
+my article was missing something that's present on the original Dawn page -- an evaluator. In this article, I'll define
+an evaluator function in Coq, prove that it's equivalent to Dawn's formal semantics,
+and extract all of this into usable Haskell code.
+
+### Changes Since Last Time
+In trying to write and verify this evaluator, I decided to make changes to the way I formalized
+the UCC. Remember how we used a predicate, `IsValue`, to tag expressions that were values?
+It turns out that this is a very cumbersome approach. For one thing, this formalization
+allows for the case in which the exact same expression is a value for two different
+reasons. Although `IsValue` has only one constructor (`Val_quote`), it's actually
+{{< sidenote "right" "hott-note" "not provable" >}}
+Interestingly, it's also not provable that any two proofs of \(a = b\) are equal,
+even though equality only has one constructor, \(\text{refl}\ :\ a \rightarrow (a = a) \).
+Under the <a href="https://homotopytypetheory.org/book/">homotopic interpretation</a>
+of type theory, this corresponds to the fact that two paths from \(a\) to \(b\) need
+not be homotopic (continuously deformable) to each other.<br>
+<br>
+As an intuitive example, imagine wrapping a string around a pole. Holding the ends of
+the string in place, there's nothing you can do to "unwrap" the string. This string
+is thus not deformable into a string that starts and stops at the same points,
+but does not go around the pole.
+{{< /sidenote >}}
+that any two proofs of `IsValue e` are equal. I ended up getting into a lot of losing
+arguments with the Coq runtime about whether or not two stacks are actually the same.
+Also, some of the semantic rules expected a value on the stack with a particular proof
+for `IsValue`, and rejected the exact same stack with a generic value.
+
+Thus, I switched from our old implementation:
+
+{{< codelines "Coq" "dawn/Dawn.v" 19 22 >}}
+
+To the one I originally had in mind:
+
+{{< codelines "Coq" "dawn/DawnV2.v" 19 19 >}}
+
+I then had the following function to convert a value back into an equivalent expression:
+
+{{< codelines "Coq" "dawn/DawnV2.v" 22 25 >}}
+
+I replaced instances of `projT1` with instances of `value_to_expr`.
+
+### Where We Are
+At the end of my previous article, we ended up with a Coq encoding of the big-step
+[operational semantics](https://en.wikipedia.org/wiki/Operational_semantics)
+of UCC, as well as some proofs of correctness about the derived forms from
+the article (like \\(\\text{quote}_3\\) and \\(\\text{rotate}_3\\)). The trouble
+is, despite having our operational semantics, we can't make our Coq
+code run anything. This is for several reasons:
+
+1. Our definitions only let us to _confirm_ that given some
+   initial stack, a program ends up in some other final stack. We even have a
+   little `Ltac2` tactic to help us automate this kind of proof. However, in an evaluator,
+   the final stack is not known until the program finishes running. We can't
+   confirm the result of evaluation, we need to _find_ it.
+2. To address the first point, we could try write a function that takes a program
+   and an initial stack, and produces a final stack, as well as a proof that
+   the program would evaluate to this stack under our semantics. However,
+   it's quite easy to write a non-terminating UCC program, whereas functions
+   in Coq _have to terminate!_ We can't write a terminating function to
+   run non-terminating code.
+
+So, is there anything we can do? No, there isn't. Writing an evaluator in Coq
+is just not possible. The end, thank you for reading.
+
+Just kidding -- there's definitely a way to get our code evaluating, but it
+will look a little bit strange.
+
+### A Step-by-Step Evaluator
+The trick is to recognize that program evaluation
+occurs in steps. There may well be an infinite number of steps, if the program
+is non-terminating, but there's always a step we can take. That is, unless
+an invalid instruction is run, like trying to clone from an empty stack, or unless
+the program finished running. You don't need a non-terminating function to just
+give you a next step, if one exists. We can write such a function in Coq.
+
+Here's a new data type that encodes the three situations we mentioned in the
+previous paragraph. Its constructors (one per case) are as follows:
+
+1. `err` - there are no possible evaluation steps due to an error.
+3. `middle e s` - the evaluation took a step; the stack changed to `s`, and the rest of the program is `e`.
+2. `final s` - there are no possible evaluation steps because the evaluation is complete, 
+leaving a final stack `s`.
+
+{{< codelines "Coq" "dawn/DawnEval.v" 6 9 >}}
+
+We can now write a function that tries to execute a single step given an expression.
+
+{{< codelines "Coq" "dawn/DawnEval.v" 11 27 >}}
+
+Most intrinsics, by themselves, complete after just one step. For instance, a program
+consisting solely of \\(\\text{swap}\\) will either fail (if the stack doesn't have enough
+values), or it will swap the top two values and be done. We list only "correct" cases,
+and resort to a "catch-all" case on line 26 that returns an error. The one multi-step
+intrinsic is \\(\\text{apply}\\), which can evaluate an arbitrary expression from the stack.
+In this case, the "one step" consists of popping the quoted value from the stack; the
+"remaining program" is precisely the expression that was popped.
+
+Quoting an expression also always completes in one step (it simply places the quoted
+expression on the stack). The really interesting case is composition. Expressions
+are evaluated left-to-right, so we first determine what kind of step the left expression (`e1`)
+can take. We may need more than one step to finish up with `e1`, so there's a good chance it
+returns a "rest program" `e1'` and a stack `vs'`. If this happens, to complete evaluation of
+\\(e_1\\ e_2\\), we need to first finish evaluating \\(e_1'\\), and then evaluate \\(e_2\\).
+Thus, the "rest of the program" is \\(e_1'\\ e_2\\), or `e_comp e1' e2`. On the other hand,
+if `e1` finished evaluating, we still need to evaluate `e2`, so our "rest of the program"
+is \\(e_2\\), or `e2`. If evaluating `e1` led to an error, then so did evaluating `e_comp e1 e2`,
+and we return `err`.
+
+### Extracting Code
+Just knowing a single step is not enough to run the code. We need something that repeatedly
+tries to take a step, as long as it's possible. However, this part is once again
+not possible in Coq, as it brings back the possibility of non-termination. So if we can't use
+Coq, why don't we use another language? Coq's extraction mechanism allows us to do just that.
+
+I added the following code to the end of my file:
+
+{{< codelines "Coq" "dawn/DawnEval.v" 231 235 >}}
+
+Coq happily produces a new file, `UccGen.hs` with a lot of code. It's not exactly the most
+aesthetic; here's a quick peek:
+
+```Haskell
+data Intrinsic =
+   Swap
+ | Clone
+ | Drop
+ | Quote
+ | Compose
+ | Apply
+
+data Expr =
+   E_int Intrinsic
+ | E_quote Expr
+ | E_comp Expr Expr
+
+data Value =
+   V_quote Expr
+
+-- ... more
+```
+
+All that's left is to make a new file, `Ucc.hs`. I use a different file so that
+Coq doesn't overwrite my changes every time I re-run extraction. In this
+file, we place the "glue code" that tries running one step after another:
+
+{{< codelines "Coq" "dawn/Ucc.hs" 46 51 >}}
+
+Finally, loading up GHCi using `ghci Ucc.hs`, I can run the following commands:
+
+```
+ghci> fromList = foldl1 E_comp
+ghci> test = eval [] $ fromList [true, false, UccGen.or]
+ghci> :f test
+test = Just [V_quote (E_comp (E_int Swap) (E_int Drop))]
+```
+
+That is, applying `or` to `true` and `false` results a stack with only `true` on top.
+As expected, and proven by our semantics!
+
+### Proving Equivalence
+Okay, so `true false or` evaluates to `true`, much like our semantics claims.
+However, does our evaluator _always_ match the semantics? So far, we have not
+claimed or verified that it does. Let's try giving it a shot.
+
+#### First Steps and Evaluation Chains
+The first thing we can do is show that if we have a proof that `e` takes
+initial stack `vs` to final stack `vs'`, then each
+`eval_step` "makes progress" towards `vs'` (it doesn't simply _return_
+`vs'`, since it only takes a single step and doesn't always complete
+the evaluation). We also want to show that if the semantics dictates
+`e` finishes in stack `vs'`, then `eval_step` will never return an error.
+Thus, we have two possibilities:
+
+* `eval_step` returns `final`. In this case, for it to match our semantics,
+  the final stack must be the same as `vs'`. Here's the relevant section
+  from the Coq file:
+
+  {{< codelines "Coq" "dawn/DawnEval.v" 30 30 >}}
+* `eval_step` returns `middle`. In this case, the "rest of the program" needs
+  to evaluate to `vs'` according to our semantics (otherwise, taking a step
+  has changed the program's final outcome, which should not happen).
+  We need to quantify the new variables (specifically, the "rest of the
+  program", which we'll call `ei`, and the "stack after one step", `vsi`),
+  for which we use Coq's `exists` clause. The whole relevant statement is as
+  follows:
+
+  {{< codelines "Coq" "dawn/DawnEval.v" 31 33 >}}
+
+The whole theorem statement is as follows:
+
+{{< codelines "Coq" "dawn/DawnEval.v" 29 33 >}}
+
+I have the Coq proof script for this (in fact, you can click the link
+at the top of the code block to view the original source file). However,
+there's something unsatisfying about this statement. In particular,
+how do we prove that an entire sequence of steps evaluates
+to something? We'd have to examine the first step, checking if
+it's a "final" step or a "middle" step; if it's a "middle" step,
+we'd have to move on to the "rest of the program" and repeat the process.
+Each time we'd have to "retrieve" `ei` and `vsi` from `eval_step_correct`,
+and feed it back to `eval_step`.
+
+I'll do you one better: how do we even _say_ that an expression "evaluates
+step-by-step to final stack `vs'`"? For one step, we can say:
+
+```Coq
+eval_step vs e = final vs'
+```
+
+Here's a picture so you can start visualizing what it looks like. The black line represents
+a single "step".
+
+{{< figure src="coq_eval_empty.png" caption="Visual representation of a single-step evaluation." class="small" alt="Two dots connected by a line. One dot is labeled \"vs\", and the other \"vs1\"." >}}
+
+For two steps, we'd have to assert the existence of an intermediate
+expression (the "rest of the program" after the first step):
+
+```Coq
+exists ei vsi,
+    eval_step vs e = middle ei vsi /\ (* First step to intermediate expression. *)
+    eval_step vsi ei = final vs' (* Second step to final state. *)
+```
+
+Once again, here's a picture. I've highlighted the intermediate state, `vsi`, in
+a brighter color.
+{{< figure src="coq_eval_one.png" caption="Visual representation of a two-step evaluation." class="small" alt="Three dots connected by lines. The first dot is labeled \"vs\", the next \"vsi\", and the last \"vs1\". The second dot is highlighted." >}}
+
+For three steps:
+
+```Coq
+exists ei1 ei2 vsi1 vsi2,
+    eval_step vs e = middle ei1 vsi1 /\ (* First step to intermediate expression. *)
+    eval_step vsi1 ei1 = middle ei2 vsi2 /\ (* Second intermediate step *)
+    eval_step vsi2 ei2 = final vs' (* Second step to final state. *)
+```
+
+I can imagine that you're getting the idea, but here's one last picture:
+{{< figure src="coq_eval_two.png" caption="Visual representation of a three-step evaluation." class="small" alt="Four dots connected by lines. The first dot is labeled \"vs\", the next \"vsi1\", the one after \"vsi2\", and the last \"vs1\". The second and third dots are highlighted." >}}
+
+The Coq code for this is awful! Not only is this a lot of writing, but it also makes various
+sequences of steps have a different "shape". This way, we can't make
+proofs about evaluations of an _arbitrary_ number of steps. Not all is lost, though: if we squint
+a little at the last example (three steps), a pattern starts to emerge.
+First, let's re-arrange the `exists` quantifiers:
+
+```Coq
+exists ei1 vsi1, eval_step vs e = middle ei1 vsi1 /\  (* Cons *)
+exists ei2 vsi2, eval_step vsi1 ei1 = middle ei2 vsi2 /\ (* Cons *)
+eval_step vsi2 ei2 = final vs' (* Nil *)
+```
+
+If you squint at this, it kind of looks like a list! The "empty"
+part of a list is the final step, while the "cons" part is a middle step. The
+analogy holds up for another reason: an "empty" sequence has zero intermediate
+expressions, while each "cons" introduces a single new intermediate
+program.
+
+{{< figure src="coq_eval_lists.png" caption="Evaluation sequences as lists." class="large" alt="The three previous figures are drawn together, each next to its list representation." >}}
+
+Perhaps we can define a new data type that matches this? Indeed
+we can!
+
+{{< codelines "Coq" "dawn/DawnEval.v" 64 67 >}}
+
+The new data type is parameterized by the initial and final stacks, as well
+as the expression that starts in the former and ends in the latter.
+Then, consider the following _type_:
+
+```Coq
+eval_chain nil (e_comp (e_comp true false) or) (true :: nil)
+```
+
+This is the type of sequences (or chains) of steps corresponding to the
+evaluation of the program \\(\\text{true}\\ \\text{false}\\ \\text{or}\\),
+starting in an empty stack and evaluating to a stack with only
+\\(\\text{true}\\) on top. Thus to say that an expression evaluates to some
+final stack `vs'`, in _some unknown number of steps_, it's sufficient to write:
+
+```Coq
+eval_chain vs e vs'
+```
+
+Evaluation chains have a couple of interesting properties. First and foremost,
+they can be "concatenated". This is analogous to the `Sem_e_comp` rule
+in our original semantics: if an expression `e1` starts in stack `vs`
+and finishes in stack `vs'`, and another expression starts in stack `vs'`
+and finishes in stack `vs''`, then we can compose these two expressions,
+and the result will start in `vs` and finish in `vs''`.
+
+{{< codelines "Coq" "dawn/DawnEval.v" 69 75 >}}
+
+{{< figure src="coq_eval_chain_merge.png" caption="Merging evaluation chains." class="large" alt="Two evaluation chains, one starting in \"vs\" and ending in \"vs'\", and one starting in \"vs'\" and ending in \"vs''\", are combined into one. The new chain starts in \"vs\", ends in \"vs''\", and has \"vs'\" in the middle. " >}}
+
+The proof is very short. We go
+{{< sidenote "right" "concat-note" "by induction on the left evaluation chain" >}}
+It's not a coincidence that defining something like <code>(++)</code>
+(list concatenation) in Haskell typically starts by pattern matching
+on the <em>left</em> list. In fact, proofs by <code>induction</code>
+actually correspond to recursive functions! It's tough putting code blocks
+in sidenotes, but if you're playing with the
+<a href="https://dev.danilafe.com/Web-Projects/blog-static/src/branch/master/code/dawn/DawnEval.v"><code>DawnEval.v</code></a> file, try running
+<code>Print eval_chain_ind</code>, and note the presence of <code>fix</code>,
+the <a href="https://en.wikipedia.org/wiki/Fixed-point_combinator">fixed point
+combinator</a> used to implement recursion.
+{{< /sidenote >}}
+(the one for `e1`). Coq takes care of most of the rest with `auto`.
+The key to this proof is that whatever `P` is contained within a "node"
+in the left chain determines how `eval_step (e_comp e1 e2)` behaves. Whether
+`e1` evaluates to `final` or `middle`, the composition evaluates to `middle`
+(a composition of two expressions cannot be done in one step), so we always
+{{< sidenote "left" "cons-note" "create a new \"cons\" node." >}}
+This is <em>unlike</em> list concatenation, since we typically don't
+create new nodes when appending to an empty list.
+{{< /sidenote >}} via `chain_middle`. Then, the two cases are as follows.
+
+If the step was `final`, then
+the rest of the steps use only `e2`, and good news, we already have a chain
+for that!
+{{< figure src="coq_eval_chain_base.png" caption="Merging evaluation chains when the first chain only has one step." class="large" alt="A single-step chain connected to another by a line labeled \"chain_middle\"." >}}
+
+Otherwise, the step was `middle`, an we still have a chain for some
+intermediate program `ei` that starts in some stack `vsi` and ends in `vs'`.
+By induction, we know that _this_ chain can be concatenated with the one
+for `e2`, resulting in a chain for `e_comp ei e2`. All that remains is to
+attach to this sub-chain the one step from `(vs, e1)` to `(vsi, ei)`, which
+is handled by `chain_middle`.
+{{< figure src="coq_eval_chain_inductive.png" caption="Merging evaluation chains when the first chain has a middle step and others." class="large" alt="Visualization of the inductive case of merging chains." >}}
+
+The `merge` operation is reversible; chains can be split into two pieces,
+one for each composed expression:
+
+{{< codelines "Coq" "dawn/DawnEval.v" 77 78 >}}
+
+While interesting, this particular fact isn't used anywhere else in this
+post, and I will omit the proof here.
+
+#### The Forward Direction
+Let's try rewording our very first proof, `eval_step_correct`, using
+chains. The _direction_ remains the same: given that an expression
+produces a final stack under the formal semantics, we need to
+prove that this expression _evaluates_ to the same final stack using
+a sequence of `eval_step`.
+
+{{< codelines "Coq" "dawn/DawnEval.v" 93 96 >}}
+
+The power of this theorem is roughly the same as that of
+the original one: we can use `eval_step_correct` to build up a chain
+by applying it over and over, and we can take the "first element"
+of a chain to serve as a witness for `eval_step_correct`. However,
+the formulation is arguably significantly cleaner, and contains
+a proof for _all_ steps right away, rather than a single one.
+
+Before we go through the proof, notice that there's actually _two_
+theorems being stated here, which depend on each other. This
+is not surprising given that our semantics are given using two
+data types, `Sem_expr` and `Sem_int`, each of which contains the other.
+Regular proofs by induction, which work on only one of the data types,
+break down because we can't make claims "by induction" about the _other_
+type. For example, while going by induction on `Sem_expr`, we run into
+issues in the `e_int` case while handling \\(\\text{apply}\\). We know
+a single step -- popping the value being run from the stack. But what then?
+The rule for \\(\\text{apply}\\) in `Sem_int` contains another `Sem_expr`
+which confirms that the quoted value properly evaluates. But this other
+`Sem_expr` isn't directly a child of the "bigger" `Sem_expr`, and so we
+don't get an inductive hypothesis about it. We know nothing about it; we're stuck.
+
+We therefore have two theorems declared together using `with` (just like we
+used `with` to declare `Sem_expr` and `Sem_int`). We have to prove both,
+which is once again a surprisingly easy task thanks to Coq's `auto`. Let's
+start with the first theorem, the one for expression semantics.
+
+{{< codelines "Coq" "dawn/DawnEval.v" 98 107 >}}
+
+We go by induction on the semantics data type. There are therefore three cases:
+intrinsics, quotes, and composition. The intrinsic case is handed right
+off to the second theorem (which we'll see momentarily). The quote case
+is very simple since quoted expressions are simply pushed onto the stack in
+a single step (we thus use `chain_final`). Finally, in the composition
+case, we have two sub-proofs, one for each expression being evaluated.
+By induction, we know that each of these sub-proofs can be turned into
+a chain, and we use `eval_chain_merge` to combine these two chains into one.
+That's it.
+
+Now, let's try the second theorem. The code is even shorter:
+
+{{< codelines "Coq" "dawn/DawnEval.v" 108 115 >}}
+
+The first command, `inversion Hsem`, lets us go case-by-case on the various
+ways an intrinsic can be evaluated. Most intrinsics are quite boring;
+in our evaluator, they only need a single step, and their semantics
+rules guarantee that the stack has the exact kind of data that the evaluator
+expects. We dismiss such cases with `apply chain_final; auto`. The only
+time this doesn't work is when we encounter the \\(\\text{apply}\\) intrinsic;
+in that case, however, we can simply use the first theorem we proved.
+
+#### A Quick Aside: Automation Using `Ltac2`
+Going in the other direction will involve lots of situations in which we _know_
+that `eval_step` evaluated to something. Here's a toy proof built around
+one such case:
+
+{{< codelines "Coq" "dawn/DawnEval.v" 237 246  "hl_lines=5-8">}}
+
+The proof claims that if the `swap` instruction was evaluated to something,
+then the initial stack must contain two values, and the final stack must
+have those two values on top but flipped. This is very easy to prove, since
+that's the exact behavior of `eval_step` for the `swap` intrinsic. However,
+notice how much boilerplate we're writing: lines 241 through 244 deal entirely
+with ensuring that our stack does, indeed, have two values. This is trivially true:
+if the stack _didn't_ have two values, it wouldn't evaluate to `final`, but to `error`.
+However, it takes some effort to convince Coq of this.
+
+This was just for a single intrinsic. What if we're trying to prove something
+for _every_ intrinsic? Things will get messy very quickly. We can't even re-use
+our `destruct vs` code, because different intrinsics need stacks with different numbers
+of values (they have a different _arity_); if we try to handle all cases with at most
+2 values on the stack, we'd have to prove the same thing twice for simpler intrinsics.
+In short, proofs will look like a mess.
+
+Things don't have to be this way, though! The boilerplate code is very repetitive, and
+this makes it a good candidate for automation. For this, Coq has `Ltac2`.
+
+In short, `Ltac2` is another mini-language contained within Coq. We can use it to put
+into code the decision making that we'd be otherwise doing on our own. For example,
+here's a tactic that checks if the current proof has a hypothesis in which
+an intrinsic is evaluated to something:
+
+{{< codelines "Coq" "dawn/DawnEval.v" 141 148 >}}
+
+`Ltac2` has a pattern matching construct much like Coq itself does, but it can
+pattern match on Coq expressions and proof goals. When pattern matching
+on goals, we use the following notation: `[ h1 : t1, ..., hn : tn |- g ]`, which reads:
+
+> Given hypotheses `h1` through `hn`, of types `t1` through `tn` respectively,
+  we need to prove `g`.
+
+In our pattern match, then, we're ignoring the actual thing we're supposed to prove
+(the tactic we're writing won't be that smart; its user -- ourselves -- will need
+to know when to use it). We are, however, searching for a hypothesis in the form
+`eval_step ?a (e_int ?b) = ?c`. The three variables, `?a`, `?b`, and `?c` are placeholders
+which can be matched with anything. Thus, we expect any hypothesis in which
+an intrinsic is evaluated to anything else (by the way, Coq checks all hypotheses one-by-one,
+starting at the most recent and finishing with the oldest). The code on lines 144 through 146 actually
+performs the `destruct` calls, as well as the `inversion` attempts that complete
+any proofs with an inconsistent assumption (like `err = final vs'`).
+
+So how do these lines work? Well, first we need to get a handle on the hypothesis we found.
+Various tactics can manipulate the proof state, and cause hypotheses to disappear;
+by calling `Control.hyp` on `h`, we secure a more permanent hold on our evaluation assumption.
+In the next line, we call _another_ `Ltac2` function, `destruct_int_stack`, which unpacks
+the stack exactly as many times as necessary. We'll look at this function in a moment.
+Finally, we use regular old tactics. Specifically, we use `inversion` (as mentioned before).
+I use `fail` after `inversion` to avoid cluttering the proof in case there's _not_
+a contradiction.
+
+On to `destruct_int_stack`. The definition is very simple:
+
+{{< codelines "Coq" "dawn/DawnEval.v" 139 139 >}}
+
+The main novelty is that this function takes two arguments, both of which are Coq expressions:
+`int`, or the intrinsic being evaluated, and `va`, the stack that's being analyzed. The `constr`
+type in Coq holds terms. Let's look at `int_arity` next:
+
+{{< codelines "Coq" "dawn/DawnEval.v" 128 137 >}}
+
+This is a pretty standard pattern match that assigns to each expression its arity. However, we're
+case analyzing over _literally any possible Coq expression_, so we need to handle the case in which
+the expression isn't actually a specific intrinsic. For this, we use `Control.throw` with
+the `Not_intrinsic` exception.
+
+Wait a moment, does Coq just happen to include a `Not_intrinsic` exception? No, it does not.
+We have to register that one ourselves. In `Ltac2`, the type of exception (`exn`) is _extensible_,
+which means we can add on to it. We add just a single constructor with no arguments:
+
+{{< codelines "Coq" "dawn/DawnEval.v" 118 118 >}}
+
+Finally, unpacking the value stack. Here's the code for that:
+
+{{< codelines "Coq" "dawn/DawnEval.v" 120 126 >}}
+
+This function accepts the arity of an operation, and unpacks the stack that many times.
+`Ltac2` doesn't have a way to pattern match on numbers, so we resort to good old "less than or equal",
+and and `if`/`else`. If the arity is zero (or less than zero, since it's an integer), we don't
+need to unpack anymore. This is our base case. Otherwise, we generate two new free variables
+(we can't just hardcode `v1` and `v2`, since they may be in use elsewhere in the proof). To this
+end we use `Fresh.in_goal` and give it a "base symbol" to build on. We then use
+`destruct`, passing it our "scrutinee" (the expression being destructed) and the names
+we generated for its components. This generates multiple goals; the `Control.enter` tactic
+is used to run code for each one of these goals. In the non-empty list case, we try to break
+apart its tail as necessary by recursively calling `destruct_n`.
+
+That's pretty much it! We can now use our tactic from Coq like any other. Rewriting
+our earlier proof about \\(\\text{swap}\\), we now only need to handle the valid case:
+
+{{< codelines "Coq" "dawn/DawnEval.v" 248 254 >}}
+
+We'll be using this new `ensure_valid_stack` tactic in our subsequent proofs.
+
+#### The Backward Direction
+After our last proof before the `Ltac2` diversion, we know that our evaluator matches our semantics, but only when a `Sem_expr`
+object exists for our program. However, invalid programs don't have a `Sem_expr` object
+(there's no way to prove that they evaluate to anything). Does our evaluator behave
+properly on "bad" programs, too? We've not ruled out that our evaluator produces junk
+`final` or `middle` outputs whenever it encounters an error. We need another theorem:
+
+{{< codelines "Coq" "dawn/DawnEval.v" 215 216 >}}
+
+That is, if our evalutor reaches a final state, this state matches our semantics.
+This proof is most conveniently split into two pieces. The first piece says that
+if our evaluator completes in a single step, then this step matches our semantics.
+
+{{< codelines "Coq" "dawn/DawnEval.v" 158 175 >}}
+
+The statement for a non-`final` step is more involved; the one step by itself need
+not match the semantics, since it only carries out a part of a computation. However,
+we _can_ say that if the "rest of the program" matches the semantics, then so does
+the whole expression.
+
+{{< codelines "Coq" "dawn/DawnEval.v" 177 213 >}}
+
+Finally, we snap these two pieces together in `eval_step_sem_back`:
+
+{{< codelines "Coq" "dawn/DawnEval.v" 215 222 >}}
+
+We have now proved complete equivalence: our evaluator completes in a final state
+if and only if our semantics lead to this same final state. As a corollary of this,
+we can see that if a program is invalid (it doesn't evaluate to anything under our semantics),
+then our evaluator won't finish in a `final` state:
+
+{{< codelines "Coq" "dawn/DawnEval.v" 224 229 >}}
+
+### Making a Mini-REPL
+We can now be pretty confident about our evaluator. However, this whole business with using GHCi
+to run our programs is rather inconvenient; I'd rather write `[drop]` than `E_quote (E_int Drop)`.
+I'd also rather _read_ the former instead of the latter. We can do some work in Haskell to make
+playing with our interpreter more convenient.
+
+#### Pretty Printing Code
+Coq generated Haskell data types that correspond precisely to the data types we defined for our
+proofs. We can use the standard type class mechanism in Haskell to define how they should be
+printed:
+
+{{< codelines "Haskell" "dawn/Ucc.hs" 8 22 >}}
+
+Now our expressions and values print a lot nicer:
+
+```
+ghci> true
+[swap drop]
+ghci> false
+[drop]
+ghci> UccGen.or
+clone apply
+```
+
+#### Reading Code In
+The Parsec library in Haskell can be used to convert text back into data structures.
+It's not too hard to create a parser for UCC:
+
+{{< codelines "Haskell" "dawn/Ucc.hs" 24 44 >}}
+
+Now, `parseExpression` can be used to read code:
+
+```
+ghci> parseExpression "[drop] [drop]"
+Right [drop] [drop]
+```
+
+#### The REPL
+We now literally have the three pieces of a read-evaluate-print loop. All that's left
+is putting them together:
+
+{{< codelines "Haskell" "dawn/Ucc.hs" 53 64 >}}
+
+We now have our own little verified evaluator:
+
+```
+$ ghci Ucc
+$ ghc -main-is Ucc Ucc
+$ ./Ucc
+> [drop] [drop] clone apply
+[[drop]]
+> [drop] [swap drop] clone apply
+[[swap drop]]
+> [swap drop] [drop] clone apply
+[[swap drop]]
+> [swap drop] [swap drop] clone apply
+[[swap drop]]
+```
+
+### Potential Future Work
+We now have a verified UCC evaluator in Haskell. What next?
+
+1. We only verified the evaluation component of our REPL. In fact,
+   the whole thing is technically a bit buggy due to the parser:
+   ```
+   > [drop] drop coq is a weird name to say out loud in interviews
+   []
+   ```
+   Shouldn't this be an error? Do you see why it's not? There's work in
+   writing formally verified parsers; some time ago I saw a Galois
+   talk about a [formally verified parser generator](https://galois.com/blog/2019/09/tech-talk-a-verified-ll1-parser-generator/).
+   We could use this formally verified parser generator to create our parsers, and then be
+   sure that our grammar is precisely followed.
+2. We could try make our evaluator a bit smarter. One thing we could definitely do
+   is maker our REPL support variables. Then, we would be able to write:
+   ```
+   > true = [swap drop]
+   > false = [drop]
+   > or = clone apply
+   > true false or
+   [swap drop]
+   ```
+   There are different ways to go about this. One way is to extend our `expr` data type
+   with a variable constructor. This would complicate the semantics (a _lot_), but it would
+   allow us to prove facts about variables. Alternatively, we could implement expressions
+   as syntax sugar in our parser. Using a variable would be the same as simply
+   pasting in the variable's definition. This is pretty much what the Dawn article
+   seems to be doing.
+3. We could prove more things. Can we confirm, once and for all, the correctness of \\(\\text{quote}_n\\),
+   for _any_ \\(n\\)? Is there is a generalized way of converting inductive data types into a UCC encoding?
+   Or could we perhaps formally verify the following comment from Lobsters:
+
+   > with the encoding of natural numbers given, n+1 contains the definition of n duplicated two times.
+     This means that the encoding of n has size exponential in n, which seems extremely impractical. 
+   
+   The world's our oyster!
+
+Despite all of these exciting possibilities, this is where I stop, for now. I hope you enjoyed this article,
+and thank you for reading!
--- a/content/blog/coq_docs/index.md
+++ b/content/blog/coq_docs/index.md
@@ -0,0 +1,84 @@
+---
+title: "I Don't Like Coq's Documentation"
+date: 2021-11-24T21:48:59-08:00
+expirydate: 2021-11-24T21:48:59-08:00
+draft: true
+tags: ["Coq"]
+---
+
+Recently, I wrote an article on [Formalizing Dawn's Core Calculus in Coq]({{< relref "./coq_dawn.md" >}}).
+One of the proofs (specifically, correctness of \\(\\text{quote}_3\\)) was the best candidate I've ever
+encountered for proof automation. I knew that proof automation was possible from the second book of Software
+Foundations, [Programming Language Foundations](https://softwarefoundations.cis.upenn.edu/plf-current/index.html).
+I went there to learn more, and started my little journey in picking up Coq's `Ltac2`.
+
+Before I go any further, let me say that I'd self-describe as an "advanced beginner" in Coq, maybe "intermediate"
+on a good day. I am certainly far from a master. I will also say that I am quite young, and thus possibly spoiled
+by the explosion of well-documented languages, tools, and libraries. I don't frequently check `man` pages, and I don't
+often read straight up technical manuals. Maybe the fault lies with me.
+Nevertheles, I feel like I am where I am in the process of learning Coq
+in part because of the state of its learning resources.
+As a case study, let's take my attempt to automate away a pretty simple proof.
+
+### Grammars instead of Examples
+I did not specifically remember the chapter of Software Foundation in which tactics were introduced.
+Instead of skimming through chapters until I found it, I tried to look up "coq custom tactic". The
+first thing that comes up is the page for `Ltac`.
+
+After a brief explanation of what `Ltac` is, the documentation jumps straight into the grammar of the entire
+tactic language. Here' a screenshot of what that looks like:
+
+{{< figure src="ltac_grammar.png" caption="The grammar of Ltac from the Coq page." class="large" alt="A grammar for the `Ltac` language within Coq. The grammar is in Backus–Naur form, and has 9 nonterminals." >}}
+
+Good old Backus-Naur form. Now, my two main areas of interest are programming language theory and compilers, and so I'm no stranger to BNF. In fact, the first
+time I saw such a documentation page (most pages describing Coq language feature have some production rules), I didn't even consciously process that I was looking
+at grammar rules. However, and despite CompCert (a compiler) being probably the most well known example of a project in Coq, I don't think that Coq is made _just_
+for people familiar with PLT or compilers. I don't think it should be expected for the average newcomer to Coq (or the average beginner-ish person like me) to know how to read production rules, or to know
+what terminals and nonterminals are. Logical Founadtions sure managed to explain Gallina without resorting to BNFs.
+
+And even if I, as a newcomer, know what BNF is, and how to read the rules, there's another layer to this specification:
+the precedence of various operators is encoded in the BNF rules. This is a pretty common pattern
+for writing down programming language grammars; for each level of operator precedence, there's another
+nonterminal. We have `ltac_expr4` for sequencing (the least binding operator), and `ltac_expr3` for "level 3 tactics",
+`ltac_expr2` for addition, logical "or", and "level 2 tactics". The creators of this documentation page clearly knew
+what they were getting at here, and I've seen this pattern enough times to recognize it right away. But if you
+_haven't_ seen this pattern before (and why should you have?), you'll need to take some time to decipher the rules.
+That's time that you'd rather spend trying to write your tactic.
+
+The page could just as well have mentioned the types of constructs in `Ltac`, and given a table of their relative precedence.
+This could be an opportunity to give an example of what a program in `Ltac` looks like. Instead, despite having seen all of these nonterminals,
+I still don't have an image in my mind's eye of what the language looks like. And better yet, I think that the grammar's incorrect:
+
+```
+ltac_expr4 ::= ltac_expr3 ; ltac_expr3|binder_tactic
+```
+
+The way this is written, there's no way to sequence (using a semicolon) more than two things. The semicolon
+only occurs on level four, and both nonterminals in this rule are level three. However, Coq is perfectly happy
+to accept the following:
+
+```Coq
+Ltac test := auto; auto; auto.
+```
+
+In the `Ltac2` grammar, this is written the way I'd expect:
+
+```
+ltac2_expr ::= ltac2_expr5 ; ltac2_expr
+```
+
+Let's do a quick recap. We have an encoding that requires a degree of experience with grammars and
+programming languages to be useful to the reader, _and_ this encoding
+{{< sidenote "right" "errors-note" "leaves room for errors," >}}
+Here's a question to ponder: how come this error has gone unnoticed? Surely
+people used this page to learn <code>Ltac</code>. I believe that part of the reason is
+pattern matching: an experienced reader will recognize the "precedence trick", and quickly
+scan the grammar levels to estblish precedence. The people writing and proofreading this
+documentation likely read it this way, too.
+{{< /sidenote >}}
+errors that _actually appear in practice_.
+{{< sidenote "left" "achilles-note" "We have a very precise, yet incorrect definition." >}}
+Amusingly, I think this is very close to what is considered the achilles heel of formal verification:
+software that precisely adheres to an incorrect or incomplete specification.
+{{< /sidenote >}}
+Somehow, "a sequence of statements separated by a semicolon" seems like a simpler explanation.
--- a/content/blog/coq_docs/ltac_grammar.png
+++ b/content/blog/coq_docs/ltac_grammar.png
--- a/content/blog/typesafe_imperative_lang.md
+++ b/content/blog/typesafe_imperative_lang.md
@@ -1,7 +1,7 @@
 ---
 title: "A Typesafe Representation of an Imperative Language"
 date: 2020-11-02T01:07:21-08:00
-tags: ["Idris"]
+tags: ["Idris", "Programming Languages"]
 ---

 A recent homework assignment for my university's programming languages
--- a/content/blog/typesafe_interpreter.md
+++ b/content/blog/typesafe_interpreter.md
@@ -1,7 +1,7 @@
 ---
 title: Meaningfully Typechecking a Language in Idris
 date: 2020-02-27T21:58:55-08:00
-tags: ["Haskell", "Idris"]
+tags: ["Haskell", "Idris", "Programming Languages"]
 ---

 This term, I'm a TA for Oregon State University's Programming Languages course.
--- a/content/blog/typesafe_interpreter_revisited.md
+++ b/content/blog/typesafe_interpreter_revisited.md
@@ -1,7 +1,7 @@
 ---
 title: Meaningfully Typechecking a Language in Idris, Revisited
 date: 2020-07-22T14:37:35-07:00
-tags: ["Idris"]
+tags: ["Idris", "Programming Languages"]
 favorite: true
 ---

--- a/content/blog/typesafe_interpreter_tuples.md
+++ b/content/blog/typesafe_interpreter_tuples.md
@@ -1,7 +1,7 @@
 ---
 title: Meaningfully Typechecking a Language in Idris, With Tuples
 date: 2020-08-12T15:48:04-07:00
-tags: ["Idris"]
+tags: ["Idris", "Programming Languages"]
 ---

 Some time ago, I wrote a post titled
--- a/content/blog/typescript_typesafe_events.md
+++ b/content/blog/typescript_typesafe_events.md
@@ -0,0 +1,120 @@
+---
+title: "Type-Safe Event Emitter in TypeScript"
+date: 2021-09-04T17:18:49-07:00
+tags: ["TypeScript"]
+---
+
+I've been playing around with TypeScript recently, and enjoying it too.
+Nearly all of my compile-time type safety desires have been accomodated
+by the language, and in a rather intuitive and clean way. Today, I'm going
+to share a little trick I've discovered which allows me to do something that
+I suspect would normally require [dependent types](https://en.wikipedia.org/wiki/Dependent_type).
+
+### The Problem
+Suppose you want to write a class that emits events. Clients can then install handlers,
+functions that are notified whenever an event is emitted. Easy enough; in JavaScript,
+this would look something like the following:
+
+{{< codelines "JavaScript" "typescript-emitter/js1.js" 1 17 >}}
+
+We can even write some code to test that this works (just to ease my nerves):
+
+{{< codelines "JavaScript" "typescript-emitter/js1.js" 19 23 >}}
+
+As expected, we get:
+
+```
+Ended!
+Started!
+```
+
+As you probably guessed, we're going to build on this problem a little bit.
+In certain situations, you don't just care that an event occured; you also
+care about additional event data. For instance, when a number changes, you
+may want to know the number's new value. In JavaScript, this is a trivial change:
+
+{{< codelines "JavaScript" "typescript-emitter/js2.js" 1 17 "hl_lines = 6-8" >}}
+
+That's literally it. Once again, let's ensure that this works by sending two new events:
+`stringChange` and `numberChange`.
+
+{{< codelines "JavaScript" "typescript-emitter/js2.js" 19 23 >}}
+
+The result of this code is once again unsurprising:
+
+```
+New number value is:  1
+New string value is:  3
+```
+
+But now, how would one go about encoding this in TypeScript? In particular, what is the
+type of a handler? We could, of course, give each handler the type `(value: any) => void`.
+This, however, makes handlers unsafe. We could very easily write:
+
+```TypeScript
+emitter.addHandler("numberChanged", (value: string) => {
+    console.log("String length is", value.length);
+});
+emitted.emit("numberChanged", 1);
+```
+
+Which would print out:
+
+```
+String length is undefined
+```
+
+No, I don't like this. TypeScript is supposed to be all about adding type safety to our code,
+and this is not at all type safe. We could do all sorts of weird things! There is a way,
+however, to make this use case work.
+
+### The Solution
+
+Let me show you what I came up with:
+
+{{< codelines "TypeScript" "typescript-emitter/ts.ts" 1 19 "hl_lines=1 2 8 12">}}
+
+The important changes are on lines 1, 2, 8, and 12 (highlighted in the above code block).
+Let's go through each one of them step-by-step.
+
+* __Line 1__: Parameterize the `EventEmitter` by some type `T`. We will use this type `T`
+  to specify the exact kind of events that our `EventEmitter` will be able to emit and handle.
+  Specifically, this type will be in the form `{ event: EventValueType }`. For example,
+  for a `mouseClick` event, we may write `{ mouseClick: { x: number, y: number }}`.
+* __Line 2__: Add a proper type to `handlers`. This requires several ingredients of its own:
+  * We use [index signatures](https://www.typescriptlang.org/docs/handbook/2/objects.html#index-signatures)
+    to limit the possible names to which handlers can be assigned. We limit these names
+    to the keys of our type `T`; in the preceding example, `keyof T` would be `"mouseClick"`.
+  * We also limit the values: `T[eventName]` retrieves the type of the value associated with
+    key `eventName`. In the mouse example, this type would be `{ x: number, y: number }`. We require
+    that a key can only be associated with an array of functions to void, each of which accepts
+    `T[K]` as first argument. This is precisely what we want; for example, `mouseClick` would map to
+    an array of functions that accept the mouse click location.
+* __Line 8__: We restrict the type of `emit` to only accept values that correspond to the keys
+  of the type `T`. We can't simply write `event: keyof T`, because this would not give us enough
+  information to retrieve the type of `value`: if `event` is just `keyof T`,
+  then `value` can be any of the values of `T`. Instead, we use generics; this way, when the
+  function is called with `"mouseClick"`, the type of `K` is inferred to also be `"mouseClick"`, which
+  gives TypeScript enough information to narrow the type of `value`.
+* __Line 12__: We use the exact same trick here as we did on line 8.
+
+Let's give this a spin with our `numberChange`/`stringChange` example from earlier:
+
+{{< codelines "TypeScript" "typescript-emitter/ts.ts" 21 27 >}}
+
+The function calls on lines 24 and 25 are correct, but the subsequent two (on lines 26 and 27)
+are not, as they attempt to emit the _opposite_ type of the one they're supposed to. And indeed,
+TypeScript complains about only these two lines:
+
+```
+code/typescript-emitter/ts.ts:26:30 - error TS2345: Argument of type 'string' is not assignable to parameter of type 'number'.
+26 emitter.emit("numberChange", "1");
+                                ~~~
+code/typescript-emitter/ts.ts:27:30 - error TS2345: Argument of type 'number' is not assignable to parameter of type 'string'.
+27 emitter.emit("stringChange", 3);
+                                ~
+Found 2 errors.
+```
+
+And there you have it! This approach is now also in use in [Hydrogen](https://github.com/vector-im/hydrogen-web),
+a lightweight chat client for the [Matrix](https://matrix.org/) protocol. In particular, check out [`EventEmitter.ts`](https://github.com/vector-im/hydrogen-web/blob/master/src/utils/EventEmitter.ts).
--- a/static/Resume-Danila-Fedorin.pdf
+++ b/static/Resume-Danila-Fedorin.pdf
--- a/static/index.st
+++ b/static/index.st
Author	SHA1	Message	Date
Danila Fedorin	13aef5b3c0	Edit and publish second Coq Dawn article	2021-12-02 18:29:47 -08:00
Danila Fedorin	b8f9f93537	Add illustrations about evaluation chains	2021-12-02 17:41:36 -08:00
Danila Fedorin	1c93d28441	Remove undercore from refl constructor to avoid KaTeX errors	2021-11-28 19:34:57 -08:00
Danila Fedorin	2ce351f7ef	Actually push the rest of the new article	2021-11-28 17:33:04 -08:00
Danila Fedorin	826dde759f	Finish a draft of the UCC evaluator article	2021-11-28 16:50:28 -08:00
Danila Fedorin	d1aa966737	Temporarily hide the Coq documentation article, even from drafts.	2021-11-28 16:46:56 -08:00
Danila Fedorin	4d24e7095b	Make some more progress on the UCC evaluator article	2021-11-28 01:48:01 -08:00
Danila Fedorin	6c1940f5d2	Get started on a post about a UCC evaluator	2021-11-28 01:09:26 -08:00
Danila Fedorin	30c395151d	Use a different representation of values and prove equivalence of UCC evalutor	2021-11-28 01:08:56 -08:00
Danila Fedorin	d72e64c7f9	Fix Ltac2 bug in Dawn file	2021-11-27 23:13:08 -08:00
Danila Fedorin	abdc8e5056	Cleanup DawnEval.v	2021-11-27 14:17:09 -08:00
Danila Fedorin	bc754c7a7d	Start working on a verified UCC evaluator.	2021-11-26 01:40:04 -08:00
Danila Fedorin	84ad8d43b5	Start on a draft for rant about Coq documentation	2021-11-25 00:33:54 -08:00
Danila Fedorin	e440630497	Re-generate Stork index	2021-11-21 16:38:48 -08:00
Danila Fedorin	71689fce79	Update tags	2021-11-21 16:20:18 -08:00
Danila Fedorin	e7185ff460	Fix calling UCC Dawn	2021-11-21 12:38:19 -08:00
Danila Fedorin	18f493675a	Publish the dawn post	2021-11-20 23:36:57 -08:00
Danila Fedorin	0c004b2e85	Edit the Dawn post a bit	2021-11-20 23:36:45 -08:00
Danila Fedorin	c214d9ee37	Add the initial version of the Dawn article.	2021-11-20 23:21:03 -08:00
Danila Fedorin	72259c16a9	Update resume	2021-10-03 20:36:54 -07:00
Danila Fedorin	66b656ada5	Published TypeScript article	2021-09-19 12:34:40 -07:00
Danila Fedorin	46e4ca3948	Fix typos in TypeScript article	2021-09-19 12:30:44 -07:00
Danila Fedorin	f2bf2fb025	Fix up donation styles on smaller screens	2021-09-19 12:18:00 -07:00
Danila Fedorin	50d48deec1	Update resume	2021-09-04 19:24:40 -07:00
Danila Fedorin	3c905aa1d7	Add draft of TypeScript typesafe event emitter post	2021-09-04 18:32:08 -07:00