Make some more progress on the UCC evaluator article

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;
         }
     }
 

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.

code/dawn/DawnEval.v

@@ -0,0 +1,223 @@
+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 compoition, 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 with vs2; auto.
+  - 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 *)
+      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. *)
+    simpl in Hev. injection Hev as Hinj; subst. solve_basic ().
+  - (* Compose is never final. *)
+    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. *)
+      destruct v. inversion Hev.
+    + (* compose with two quoted values. *)
+      destruct v; destruct v0. inversion Hev.
+    + (* Apply *)
+      destruct v. injection Hev as Hinj; subst.
+      solve_basic (). auto.
+  - inversion Hev.
+  - simpl in Hev.
+    destruct (eval_step vs e1) eqn:Hev1.
+    + inversion Hev.
+    + injection Hev as Hinj; subst. inversion Hsem; subst.
+      specialize (IHe1 e vs vsi vs2 Hev1 H2).
+      eapply Sem_e_comp. apply IHe1. apply H4.
+    + injection Hev as Hinj; subst.
+      specialize (eval_step_final_sem e1 vs vsi Hev1) as Hsem1.
+      eapply Sem_e_comp. apply Hsem1. apply Hsem.
+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.

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.

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

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");

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");

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);

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.

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

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

content/blog/coq_dawn.md

@@ -0,0 +1,376 @@
+---
+title: "Formalizing Dawn in Coq"
+date: 2021-11-20T19:04:57-08:00
+tags: ["Coq", "Dawn", "Programming Languages"]
+---
+
+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.

content/blog/coq_dawn_eval.md

@@ -0,0 +1,325 @@
+---
+title: "A Verified Evaluator for the Untyped Concatenative Calculus"
+date: 2021-11-27T20:24:57-08:00
+draft: true
+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 thing 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{eq_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" 219 223 >}}
+
+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
+changes I make aren't overridden by Coq each time I 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.
+
+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 semanics 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 claim 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'
+```
+
+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. *)
+```
+
+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. *)
+```
+
+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 evalutions 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` qualifiers:
+
+```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. 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 analagous 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 >}}
+
+The proof is very short. We go
+{{< sidenote "right" "concat-note" "by induction on the left evaluation" >}}
+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 >}}
+chain (the one for `e1`). Coq takes care of most of the rest with `auto`.
+The key to this proof is that whatever `P` is cotained 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!
+* Otherwise, the step was `middle`, an we stll 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`.
+
+  {{< todo >}}A drawing would be nice here!{{< /todo >}}
+
+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.

content/blog/coq_docs/index.md

@@ -0,0 +1,83 @@
+---
+title: "I Don't Like Coq's Documentation"
+date: 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.

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

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.

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
 ---
 

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

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).