Tweak styles to make things work nicely with "page-looking things"

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
Finish draft
2026-05-22 23:22:24 -07:00 · 2026-05-22 22:48:12 -07:00 · 2026-05-22 21:01:11 -07:00 · 2026-05-19 17:55:47 -07:00 · 2026-05-19 17:06:51 -07:00 · 2026-05-19 17:05:43 -07:00
71 changed files with 3892 additions and 273 deletions
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,6 @@
 **/build/*
 .DS_Store
 /.hugo_build.lock
 /.hugo_cache/
 /public/
 /resources/
--- a/Gemfile.lock
+++ b/Gemfile.lock
@@ -3,11 +3,11 @@ GEM
  specs:
    duktape (2.7.0.0)
    execjs (2.9.1)
-    mini_portile2 (2.8.6)
+    mini_portile2 (2.8.8)
-    nokogiri (1.15.6)
+    nokogiri (1.18.3)
      mini_portile2 (~> 2.8.2)
      racc (~> 1.4)
-    racc (1.8.0)
+    racc (1.8.1)
 PLATFORMS
  ruby
--- a/agda.rb
+++ b/agda.rb
@@ -23,7 +23,7 @@ class AgdaContext
    return @file_infos[file] if @file_infos.include? file
    @file_infos[file] = line_infos = {}
-    unless File.exists?(file)
+    unless File.exist?(file)
      return line_infos
    end
@@ -46,7 +46,17 @@ class AgdaContext
          # assumes that links can't span multiple pages, and that links
          # aren't nested, so ensure that the parent of the textual node
          # is the preformatted block itself.
-          raise "unsupported Agda HTML output" if at.parent.name != "pre"
+          if at.parent.name != "pre"
            # Costmetic highlight warnings are sometimes applied to newlines.
            # If they don't have content, treat them as normal newlines at the
            # top level.
            #
            # This is an <a class="CosmeticProblem">\n</a> node.
            unless at.parent.name == "a" and at.parent['class'] == "CosmeticProblem" and at.content.strip.empty?
              raise "unsupported Agda HTML output in file #{file} at line #{line} (content #{at.content.inspect})"
            end
          end
          # Increase the line and track the final offset. Written as a loop
          # in case we eventually want to add some handling for the pieces
@@ -160,6 +170,14 @@ class FileGroup
        line_range = 1..
      end
      # Sometimes, code is deeply nested in the source file, but we don't
      # want to show the leading space. In that case, the generator sets
      # data-source-offset with how much leading space was stripped off.
      initial_offset = 0
      if source_offset_attr = t.attribute("data-source-offset")
        initial_offset = source_offset_attr.to_s.to_i
      end
      full_path = t.attribute("data-file-path").to_s
      full_path_dirs = Pathname(full_path).each_filename.to_a
@@ -195,7 +213,7 @@ class FileGroup
        line_info = agda_info[line_no]
        next unless line_info
-        offset = 0
+        offset = initial_offset
        line.traverse do |lt|
          if lt.text?
            content = lt.content
--- a/analyze.rb
+++ b/analyze.rb
@@ -43,7 +43,7 @@ files.each do |file|
  tags = []
  group = 1
  draft = false
-  next unless File.exists?(file)
+  next unless File.exist?(file)
  value = File.size(file)
  url = file.gsub(/^content/, "https://danilafe.com").delete_suffix("/index.md").delete_suffix(".md")
  File.readlines(file).each do |l|
--- a/assets/scss/bergamot.scss
+++ b/assets/scss/bergamot.scss
@@ -1,174 +0,0 @@
@import "variables.scss";
@import "mixins.scss";
 .bergamot-exercise {
    counter-increment: bergamot-exercise;
    .bergamot-root {
        border: none;
        padding: 0;
        margin-top: 1em;
    }
    .bergamot-exercise-label {
        .bergamot-exercise-number::after {
            content: "Exercise " counter(bergamot-exercise);
            font-weight: bold;
            text-decoration: underline;
        }
    }
    .bergamot-button {
        @include bordered-block;
        padding: 0.25em;
        padding-left: 1em;
        padding-right: 1em;
        background-color: inherit;
        display: inline-flex;
        align-items: center;
        justify-content: center;
        transition: 0.25s;
        font-family: $font-body;
        @include var(color, text-color);
        &.bergamot-hidden {
            display: none;
        }
        .feather {
            margin-right: 0.5em;
        }
    }
    .bergamot-play {
        .feather { color: $primary-color; }
        &:hover, &:focus {
            .feather { color: lighten($primary-color, 20%); }
        }
    }
    .bergamot-reset {
        .feather { color: #0099CC; }
        &:hover, &:focus {
            .feather { color: lighten(#0099CC, 20%); }
        }
        svg {
            fill: none;
        }
    }
    .bergamot-close {
        .feather { color: tomato; }
        &:hover, &:focus {
            .feather { color: lighten(tomato, 20%); }
        }
    }
    .bergamot-button-group {
        margin-top: 1em;
    }
 }
 .bergamot-root {
    @include bordered-block;
    padding: 1em;
    .bergamot-section-heading {
        margin-bottom: 0.5em;
        font-family: $font-body;
        font-style: normal;
        font-weight: bold;
        font-size: 1.25em;
    }
    .bergamot-section {
        margin-bottom: 1em;
    }
    textarea {
        display: block;
        width: 100%;
        height: 10em;
        resize: none;
    }
    input[type="text"] {
        width: 100%;
        @include textual-input;
    }
    .bergamot-rule-list {
        display: flex;
        flex-direction: row;
        flex-wrap: wrap;
        justify-content: center;
    }
    .bergamot-rule-list katex-expression {
        margin-left: .5em;
        margin-right: .5em;
        flex-grow: 1;
        flex-basis: 0;
    }
    .bergamot-rule-section {
        .bergamot-rule-section-name {
            text-align: center;
            margin: 0.25em;
            font-weight: bold;
        }
    }
    .bergamot-proof-tree {
        overflow: auto;
    }
    .bergamot-error {
        @include bordered-block;
        padding: 0.5rem;
        border-color: tomato;
        background-color: rgba(tomato, 0.25);
        margin-top: 1rem;
    }
    .bergamot-selector {
        button {
            @include var(background-color, background-color);
            @include var(color, text-color);
            @include bordered-block;
            padding: 0.5rem;
            font-family: $font-body;
            border-style: dotted;
            &.active {
                border-color: $primary-color;
                border-style: solid;
                font-weight: bold;
            }
            &:not(:first-child) {
                border-bottom-left-radius: 0;
                border-top-left-radius: 0;
            }
            &:not(:last-child) {
                border-bottom-right-radius: 0;
                border-top-right-radius: 0;
                border-right-width: 0;
            }
        }
        button.active + button {
            border-left-color: $primary-color;
            border-left-style: solid;
        }
        margin-bottom: 1rem;
    }
    .bergamot-no-proofs {
        text-align: center;
    }
 }
--- a/assets/svg/spiderweb.svg
+++ b/assets/svg/spiderweb.svg
@@ -0,0 +1,718 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <!-- Created with Inkscape (http://www.inkscape.org/) -->
 <svg
   width="197.21727mm"
   height="106.16592mm"
   viewBox="0 0 197.21727 106.16592"
   version="1.1"
   id="svg1"
   xml:space="preserve"
   inkscape:version="1.4.2 (ebf0e940, 2025-05-08)"
   sodipodi:docname="spiderweb.svg"
   xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
   xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
   xmlns="http://www.w3.org/2000/svg"
   xmlns:svg="http://www.w3.org/2000/svg"><sodipodi:namedview
     id="namedview1"
     pagecolor="#000000"
     bordercolor="#000000"
     borderopacity="0.25"
     inkscape:showpageshadow="2"
     inkscape:pageopacity="0.0"
     inkscape:pagecheckerboard="0"
     inkscape:deskcolor="#d1d1d1"
     inkscape:document-units="mm"
     inkscape:zoom="1.2119635"
     inkscape:cx="292.91312"
     inkscape:cy="235.56816"
     inkscape:window-width="1728"
     inkscape:window-height="996"
     inkscape:window-x="0"
     inkscape:window-y="38"
     inkscape:window-maximized="1"
     inkscape:current-layer="mainlayer" /><defs
     id="defs1" /><g
     inkscape:groupmode="layer"
     id="mainlayer"
     inkscape:label="Main Layer"
     transform="translate(-12.908849,0.44133637)"><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 107.50107,0.48134806 -4.01124,4.49258204 c 0,0 5.61573,31.9294199 14.28,37.0637999 8.66426,5.134379 7.54112,5.294828 7.54112,5.294828"
       id="path2"
       sodipodi:nodetypes="ccsc" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 173.22006,0.15397339 85.91715,39.263214"
       id="path3" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 183.22833,-0.15397339 c 0,0 -49.11751,32.33441039 -64.66882,56.50823339"
       id="path4" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 185.53793,-0.30794677 c 0,0 -48.80956,45.57612277 -56.50823,61.43538277"
       id="path5" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 184.76806,4.1572814 c 0,0 -42.1887,53.8906846 -31.41057,70.2118646"
       id="path6" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 190.46508,0 c 0,0 -31.10262,53.428764 -18.93873,84.99331"
       id="path7" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 191.85084,-0.15397339 c 0,0 -17.55297,60.81948839 -3.23344,92.69197939"
       id="path8" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 193.54455,-0.15397339 c 0,0 -6.62086,54.50657839 16.32117,86.53304339"
       id="path9" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 196.31607,-0.30794677 c 0,0 6.00496,36.33771977 13.54965,48.19366877"
       id="path10" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 197.39388,0.15397339 209.86572,26.483423"
       id="path11" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 198.62567,0.30794677 209.55778,15.551312"
       id="path12" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 115.28177,0.20224871 c 0,0 -2.52811,22.24735829 -0.30337,25.68558729"
       id="path13" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 120.33799,1.415741 0.30337,11.932674 v 0 c 0,0 -1.21349,6.269711 -1.21349,10.213561"
       id="path14" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 120.64136,13.752913 c 0,0 1.92136,7.584327 2.02249,8.59557"
       id="path15" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 125.89983,0.80899486 c 0,0 0,9.50569014 5.05621,17.79788714"
       id="path16" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 126.91107,10.112436 c 0,0 -0.4045,5.865213 0.70787,10.314684"
       id="path17" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 128.63018,0.20224871 134.39427,17.494514"
       id="path18" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 135.30439,0.30337307 c 0,0 0.60675,9.91018693 2.42698,15.57315093"
       id="path19" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 139.75386,0.7078705 c 0,0 -1.41574,3.94385 1.61799,13.7529125"
       id="path20" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 143.09097,1.1123679 c 0,0 1.82024,8.3933216 3.84272,11.2248041"
       id="path21" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 144.30446,6.0674614 c 0,0 -0.809,2.9326065 -0.30337,6.7753316"
       id="path22" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 147.54044,0.40449743 148.75393,10.618058"
       id="path23" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 150.87754,0.20224871 3.43823,7.78657559"
       id="path24" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 153.2034,0.10112436 3.3371,6.37083444"
       id="path25" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 155.52926,0.20224871 3.33711,5.66296389"
       id="path26" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 159.06861,0.50562179 161.4956,4.7528448"
       id="path27" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 162.00122,0.40449743 164.02371,3.94385"
       id="path28" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 164.4282,-0.30337307 1.92137,3.33710377"
       id="path29" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 115.28177,26.797955 c 0,0 -2.02249,11.427052 11.93267,16.786643"
       id="path30" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 120.03461,24.269846 c 0,0 3.84273,11.022554 12.74167,14.86528"
       id="path31" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 126.30432,21.33724 c 0,0 0.4045,9.404565 9.00007,15.067529"
       id="path32" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 134.69765,17.797887 c 0,0 -4.85397,8.494446 5.15734,14.460782"
       id="path33" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 137.428,16.078773 c 0,0 0.30337,6.26971 5.05622,13.95516"
       id="path34" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 140.15836,14.15741 c 0,0 -1.01124,6.370835 4.75285,13.854038"
       id="path35" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 143.29321,13.045042 c 0,0 -0.91011,7.584327 4.34835,12.640545"
       id="path36" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 146.32695,12.842793 c 0,0 -2.32586,4.044975 3.13485,11.325928"
       id="path37" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 147.54044,11.427052 c 0,0 0.20225,7.17983 4.75284,10.820307"
       id="path38" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 149.76517,9.9101872 c 0,0 1.41574,8.4944458 3.94385,10.3146838"
       id="path39" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 151.58541,9.7079384 c 0,0 2.02249,6.4719586 5.25847,8.5955706"
       id="path40" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 153.2034,9.0000679 c 0,0 2.12361,5.9663371 4.85397,7.8877001"
       id="path41" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 154.31577,8.2921974 5.86521,7.0787046"
       id="path42" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 209.52546,105.56381 12.995207,0"
       id="path43" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 158.24027,7.5068802 4.05133,6.7919388"
       id="path44" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 160.24291,5.8928883 3.88494,7.1587677"
       id="path45" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 162.81832,4.4087534 3.71034,6.8968616"
       id="path46" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 165.48103,3.666686 3.01192,6.416701"
       id="path47" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 167.88184,2.4008064 2.79367,5.9365392"
       id="path48" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 171.19932,0.52381229 2.1389,5.98019051"
       id="path49" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 173.42552,0.43651024 1.70239,4.62700856"
       id="path50" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 176.17554,0.43651024 1.30953,3.14287386"
       id="path51" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 176.52474,4.6270087 1.39684,1.7460409"
       id="path52" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 174.56045,5.9365393 1.83334,1.920645"
       id="path53" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 171.85408,7.8571843 2.70637,2.0952494"
       id="path54" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 170.23899,9.4286212 2.09526,2.4881088"
       id="path55" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 167.00882,11.654823 3.49208,2.051599"
       id="path56" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 165.00087,12.702448 3.44843,2.793666"
       id="path57" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 163.25483,14.317536 3.31748,3.011921"
       id="path58" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 161.02863,15.32151 4.23415,3.797639"
       id="path59" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 158.80243,17.89692 3.75399,3.579384"
       id="path60" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 155.6159,18.900894 5.84924,4.103196"
       id="path61" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 154.48098,21.432653 5.10717,3.317478"
       id="path62" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 151.94922,22.698533 4.58335,4.845264"
       id="path63" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 149.06825,25.361245 6.19844,4.190498"
       id="path64" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 148.23888,26.539822 c 0,0 1.74604,3.492082 4.71431,5.674635"
       id="path65" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 144.57219,28.635073 c 0,0 2.35716,2.575409 6.54766,4.583356"
       id="path66" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 142.6952,30.992228 c 0,0 3.66669,4.365101 6.2421,5.019868"
       id="path67" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 138.63565,33.916847 c 0,0 4.23415,3.186523 8.25005,4.059544"
       id="path68" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 137.10787,35.008121 c 0,0 4.1905,5.89289 7.15877,6.023843"
       id="path69" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 134.88167,37.758137 c 0,0 2.79366,4.32145 6.72225,5.500028"
       id="path70" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 132.69912,39.373225 c 0,0 3.53573,5.325425 7.50797,6.111142"
       id="path71" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 130.77847,41.512124 c 0,0 3.66669,6.02384 7.20242,7.289721"
       id="path72" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 128.42131,43.781977 c 0,0 2.44446,5.369076 7.07147,6.984164"
       id="path73" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 127.06813,45.528018 c 0,0 2.70637,7.420676 6.11115,8.555601"
       id="path74" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 124.49272,48.452637 c 0,0 2.92462,6.373051 6.94051,7.988139"
       id="path75" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 182.0798,2.2845037 2.38172,2.0414713"
       id="path76" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 183.92685,5.4925301 2.2845,1.7498327 2.81918,2.0900778"
       id="path77" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 188.7875,10.110144 4.03433,-0.729097 4.71483,-1.3123744"
       id="path78" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 197.68248,7.8256402 2.38171,-0.8749163"
       id="path79" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 200.55026,5.055072 1.60401,-1.0693422"
       id="path80" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 201.6196,3.8399103 204.29296,0"
       id="path81" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 203.32083,6.9021176 c 0,0 3.35384,-2.7219619 4.18015,-6.65908529"
       id="path82" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 204.92484,8.4089178 c 0,0 3.45106,-2.2358971 4.61761,-7.3881821"
       id="path83" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 180.76743,4.4717943 1.84705,2.6247489"
       id="path84" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 182.46866,7.1451498 2.57614,2.7219619"
       id="path85" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 184.80176,10.547602 3.49967,1.992865"
       id="path86" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 188.44725,13.220958 4.37458,-0.194426"
       id="path87" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 192.67601,13.804235 5.88138,-1.992865"
       id="path88" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 198.55739,10.742028 3.0136,-1.0693422"
       id="path89" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 203.51525,7.5340016 -1.94426,1.6526195"
       id="path90" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 205.11927,9.4782599 -2.57615,2.0414711"
       id="path91" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 177.65661,7.5340016 2.43033,2.0900776"
       id="path92" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 180.23276,10.450389 3.0622,2.770569"
       id="path93" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 183.10054,14.14448 4.27737,2.381717"
       id="path94" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 188.39864,15.748494 4.13155,0.09721"
       id="path95" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 193.3079,15.991526 5.44392,-1.360981"
       id="path96" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 199.57813,15.408248 4.76343,-0.243032"
       id="path97" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 204.04992,13.220958 2.77057,-1.360981"
       id="path98" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 206.62607,10.596209 2.96499,-3.7913043"
       id="path99" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 207.74402,12.929319 1.70122,-2.284504"
       id="path100" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 175.71236,9.5754729 2.81917,2.3331101"
       id="path101" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 178.04547,13.609809 4.13155,2.867781"
       id="path102" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 182.37144,16.428984 4.81204,2.235897 5.2495,0.09721"
       id="path103" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 192.28716,18.713488 7.4854,-0.82631"
       id="path104" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 200.21001,19.296765 4.95786,-1.701226"
       id="path105" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 205.4109,15.311035 2.77057,-1.5068"
       id="path106" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 200.8419,20.852172 -7.97146,1.5068"
       id="path107" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 186.50299,22.164546 6.85351,0.194426"
       id="path108" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 180.71882,19.393978 5.83278,2.770568"
       id="path109" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 176.49006,15.408248 4.71483,3.499665"
       id="path110" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 173.96252,11.568338 2.91639,3.208026"
       id="path111" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 171.62941,13.46399 3.30524,3.15942"
       id="path112" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 174.88605,18.178817 4.76343,3.062207"
       id="path113" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 179.40645,23.039463 7.14515,2.18729"
       id="path114" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 185.87111,26.150276 6.70769,-0.534671"
       id="path115" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 200.79329,23.428314 -8.2631,2.187291"
       id="path116" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 207.74402,22.504792 c 0,0 -5.00647,2.867781 -5.88139,3.062207"
       id="path117" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 168.42139,16.185952 5.2981,2.624749"
       id="path118" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 166.91459,17.692752 4.76343,3.888517"
       id="path119" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 172.65015,20.657746 5.63835,3.402452"
       id="path120" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 178.48292,26.053063 7.04794,1.652619"
       id="path121" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 185.28783,28.726418 7.63121,-0.68049"
       id="path122" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 201.71681,26.393308 -8.79777,1.604014"
       id="path123" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 202.49452,29.066664 193.3565,31.74002"
       id="path124" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 185.23922,31.399773 8.2145,-0.14582"
       id="path125" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 176.68449,29.455514 8.65195,1.166556"
       id="path126" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 169.9768,25.858637 6.41605,3.256634"
       id="path127" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 171.09474,23.379708 c 0,0 3.93713,3.353845 6.41605,3.645484"
       id="path128" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 165.16475,20.074469 c 0,0 3.30524,3.645484 5.34672,3.985729"
       id="path129" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 162.88025,21.678482 c 0,0 4.4718,4.325975 6.56187,4.569007"
       id="path130" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 160.49853,23.914379 c 0,0 4.90926,3.791303 7.14515,4.131549"
       id="path131" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 175.42072,31.691413 c 0,0 -4.61762,-0.388853 -7.77704,-3.499665"
       id="path132" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 184.80176,33.100999 c 0,0 -7.14515,-0.194424 -9.13801,-1.604013"
       id="path133" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 184.65594,35.142471 8.79778,-1.263769"
       id="path134" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 203.32083,31.5942 -10.20736,2.478929"
       id="path135" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 166.91459,29.892974 c 0,0 -5.58975,-1.020736 -8.06868,-4.180156"
       id="path136" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 166.37992,30.524857 c 0,0 6.12441,3.548272 8.84637,3.839911"
       id="path137" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 184.51013,36.114601 c 0,0 -9.33244,-2.041472 -9.67269,-2.624749"
       id="path138" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 184.36431,37.47558 c 0,0 8.36031,-0.437457 9.0408,-0.729096"
       id="path139" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 204.34156,33.975915 c 0,0 -10.01293,3.402455 -10.83924,3.402455"
       id="path140" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 204.6332,36.211814 -11.13088,3.305238"
       id="path141" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 183.73242,41.023854 9.96433,-1.701228"
       id="path142" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 173.52507,38.544923 10.20735,2.478931"
       id="path143" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 174.4972,36.697877 9.86711,1.992866"
       id="path144" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 164.97033,33.635672 9.13801,2.867781"
       id="path145" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 156.36699,29.018058 8.94358,3.353845"
       id="path146" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 164.24123,34.899438 c 0,0 -8.3117,-2.916385 -9.18662,-5.152284"
       id="path147" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 173.71949,38.787956 c 0,0 -7.97146,-2.138685 -9.96432,-4.714827"
       id="path148" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 206.33443,38.593529 -12.20022,2.867782"
       id="path149" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 183.97545,42.530654 9.7213,-1.166556"
       id="path150" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 172.74736,42.093194 c 0,0 9.04081,1.798439 10.5476,0.923523"
       id="path151" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 162.58861,37.864433 c 0,0 7.19376,4.034338 10.15875,3.694091"
       id="path152" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 153.20756,32.12887 c 0,0 6.22163,5.881383 9.08941,5.686956"
       id="path153" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 150.72864,34.559195 c 0,0 8.11727,5.443923 10.20735,5.395317"
       id="path154" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 149.31905,35.725748 c 0,0 6.70769,7.290969 10.79063,6.075809"
       id="path155" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 171.58081,46.516382 c 0,0 -4.76344,1.749835 -11.66555,-4.277368"
       id="path156" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 183.00333,48.071791 c 0,0 -4.81204,1.117949 -11.2767,-1.701226"
       id="path157" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 194.91191,46.710808 c 0,0 -9.42965,2.819176 -11.47113,1.749833"
       id="path158" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 194.37724,43.94024 -10.74203,0.729099"
       id="path159" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 160.64435,41.995981 11.13088,2.527538"
       id="path160" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 183.19775,46.224745 171.82384,44.572126"
       id="path161" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 206.43164,41.169672 194.23142,44.08606"
       id="path162" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 207.35516,43.11393 -12.73489,3.694092"
       id="path163" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 208.08426,45.301222 195.54379,49.57859"
       id="path164" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 147.28059,37.851884 c 0,0 7.4801,7.80252 11.22015,6.448364"
       id="path165" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 145.41056,39.850877 c 0,0 5.28766,7.99597 11.86499,7.480102"
       id="path166" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 142.44432,43.139542 c 0,0 6.38387,6.899749 13.41259,7.738033"
       id="path167" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 141.15465,44.751632 c 0,0 3.09521,8.576321 12.70327,12.058439"
       id="path168" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 139.67152,46.621657 c 0,0 4.51385,13.283626 12.63879,15.991938"
       id="path169" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 137.35011,49.00755 c 0,0 8.18942,11.607054 15.41159,9.93048"
       id="path170" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 135.86699,51.071028 c 0,0 -3.67557,8.124936 15.02468,15.218135"
       id="path171" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 131.74004,56.874552 2.64383,8.124936"
       id="path172" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 146.76472,71.641302 4.57834,-2.192443"
       id="path173" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 131.4821,56.229718 5.28766,0.709318"
       id="path174" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 157.72694,45.58992 13.15465,4.320402"
       id="path175" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 157.27555,47.00856 c 0,0 9.60806,5.739043 13.15466,4.642821"
       id="path176" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 156.56623,49.00755 c 0,0 6.19043,5.739043 12.83224,5.15869"
       id="path177" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 154.88966,53.198987 14.63778,4.062468"
       id="path178" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 168.94708,63.387398 c 0,0 -13.67052,-6.319393 -14.31536,-11.284633"
       id="path179" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 169.14053,59.840799 161.85389,59.32493"
       id="path180" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 153.5355,56.874552 c 0,0 3.35315,5.094208 14.89572,9.479092"
       id="path181" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 151.66548,63.838785 c 0,0 13.79949,6.254911 16.83022,5.287655"
       id="path182" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 168.68915,72.28614 c 0,0 -17.41058,-2.127962 -17.99093,-4.126953"
       id="path183" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 170.62366,49.910322 c 0,0 11.60705,2.450378 13.02569,1.354156"
       id="path184" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 170.04331,55.971783 c 0,0 6.83526,-1.289674 12.70327,0.902769"
       id="path185" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 183.52038,55.907299 c 0,0 12.18741,-0.644837 12.63879,-1.547606"
       id="path186" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 182.87555,49.587903 c 0,0 12.76775,1.998994 13.15465,3.095215"
       id="path187" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 170.23676,51.457928 c 0,0 4.3204,-0.19345 5.22317,0.902772 0.90277,1.096221 6.06146,2.063475 7.22217,0.902771"
       id="path188" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 183.32693,52.038281 4.25592,-1.547606"
       id="path189" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 190.87151,50.619641 4.19144,-1.354156"
       id="path190" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 196.61056,54.295209 c 0,0 12.50982,-5.868011 13.34811,-3.933503"
       id="path191" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 195.12744,52.16725 c 0,0 14.18639,-0.515869 14.63778,-3.997987"
       id="path192" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 169.72089,57.841808 c 0,0 11.67153,3.159696 13.15466,1.547606"
       id="path193" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 197.31988,56.939036 -14.37985,3.288665"
       id="path194" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 197.77126,60.356667 c 0,0 -9.4146,-0.451384 -9.67254,-1.354156"
       id="path195" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 169.2695,61.517373 c 0,0 13.28363,0 13.67053,1.22519"
       id="path196" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 168.81812,64.161201 c 0,0 5.93249,-0.902769 14.37985,1.354156"
       id="path197" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 168.36673,67.965735 14.89572,0.967255"
       id="path198" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 169.39847,73.769261 13.7995,-2.192443"
       id="path199" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 168.23777,71.641302 c 0,0 1.48312,5.674559 15.92745,2.643828"
       id="path200" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 169.33399,76.735508 c 0,0 7.0932,-0.773803 14.31536,10.833248"
       id="path201" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 184.74557,76.671024 -8.96322,2.192443"
       id="path202" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 184.55212,79.766238 177.26547,79.44382"
       id="path203" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 162.11182,80.346591 7.35113,-2.966246"
       id="path204" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 165.27152,82.023166 4.12695,-2.256928"
       id="path205" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 171.07504,82.539035 c 0,0 14.25089,-0.128969 14.63779,1.870024"
       id="path206" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 180.74759,89.890168 c 0,0 4.90075,-3.417634 5.99698,-2.256928"
       id="path207" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 182.87555,67.901253 15.60503,-4.642821"
       id="path208" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 199.44784,65.773294 c 0,0 -15.21814,2.837278 -15.66952,2.837278"
       id="path209" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 182.94003,71.899237 17.3461,-3.224181"
       id="path210" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 183.52038,73.640296 201.5758,70.996465"
       id="path211" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 183.71383,77.444827 202.3496,73.575811"
       id="path212" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 185.06799,80.153141 c 0,0 19.47405,-2.063477 21.08614,-0.128968"
       id="path213" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 203.70376,77.057926 -7.02872,2.385894"
       id="path214" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 186.35766,85.440797 c 0,0 9.67254,2.450377 13.54156,1.80554"
       id="path215" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 188.1632,90.470518 209.37831,86.02115"
       id="path216" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 186.6156,87.568756 c 0,0 17.34609,-2.127959 20.44131,-3.804534"
       id="path217" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 197.70678,57.068005 12.25189,-2.966246"
       id="path218" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 198.09368,60.55012 11.86499,-3.804534"
       id="path219" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 199.06094,62.613595 10.63979,-2.643828"
       id="path220" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 199.77026,65.773294 c 0,0 8.83425,-4.255921 9.8015,-3.546599"
       id="path221" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 200.86648,68.610572 c 0,0 4.38488,1.354156 8.83425,-1.483122"
       id="path222" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 201.70476,71.060949 2.32141,-2.063474"
       id="path223" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 202.99444,74.220646 6.96423,-3.030728"
       id="path224" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 205.1224,79.314854 4.64282,-2.64383"
       id="path225" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="m 208.34658,83.635256 1.41864,-0.838287"
       id="path226" /><path
       style="fill:none;stroke:#ffffff;stroke-width:0.365;stroke-dasharray:none;stroke-opacity:1"
       d="M 29.690113,9.1690057 175.30265,0"
       id="path227" /></g></svg>
--- a/build-agda-html.rb
+++ b/build-agda-html.rb
@@ -26,7 +26,7 @@ files = ARGV
 code_paths = Dir.entries(root_path).select do |f|
  File.directory?(File.join(root_path, f)) and f != '.' and f != '..'
 end.to_set
-code_paths += JSON.parse(File.read(data_file)).keys if File.exists? data_file
+code_paths += JSON.parse(File.read(data_file)).keys if File.exist? data_file
 # Extending code_paths from submodules.json means that nested Agda modules
 # have their root dir correctly set.
--- a/chatgpt-subset-feather-icon.rb
+++ b/chatgpt-subset-feather-icon.rb
@@ -0,0 +1,49 @@
 #!/usr/bin/env ruby
 # frozen_string_literal: true
 require 'nokogiri'
 require 'set'
 # 1) Process all files passed in from the command line
 svgpath = ARGV[0]
 files = ARGV[1..]
 # 2) Extract used Feather icons
 used_icons = Set.new
 files.each do |file|
  # Parse each HTML file
  doc = File.open(file, "r:UTF-8") { |f| Nokogiri::HTML(f) }
  # Look for <use xlink:href="/feather-sprite.svg#iconName">
  doc.css("use").each do |use_tag|
    href = use_tag["xlink:href"] || use_tag["href"]
    if href && href.start_with?("/feather-sprite.svg#")
      icon_name = href.split("#").last
      used_icons << icon_name
    end
  end
 end
 puts "Found #{used_icons.size} unique icons: #{used_icons.to_a.join(', ')}"
 # 3) Load the full feather-sprite.svg as XML
 sprite_doc = File.open(svgpath, "r:UTF-8") { |f| Nokogiri::XML(f) }
 # 4) Create a new SVG with only the required symbols
 new_svg = Nokogiri::XML::Document.new
 svg_tag = Nokogiri::XML::Node.new("svg", new_svg)
 svg_tag["xmlns"] = "http://www.w3.org/2000/svg"
 new_svg.add_child(svg_tag)
 sprite_doc.css("symbol").each do |symbol_node|
  if used_icons.include?(symbol_node["id"])
    # Duplicate the symbol node (so it can be inserted in the new document)
    svg_tag.add_child(symbol_node.dup)
  end
 end
 # 5) Save the subset sprite
 File.open(svgpath, "w:UTF-8") do |f|
  f.write(new_svg.to_xml)
 end
--- a/chatgpt-subset-one-go.py
+++ b/chatgpt-subset-one-go.py
@@ -0,0 +1,69 @@
 import os
 import sys
 from bs4 import BeautifulSoup
 from fontTools.subset import Subsetter, Options
 from fontTools.ttLib import TTFont
 FONT_EXTENSIONS = (".ttf", ".woff", ".woff2", ".otf")  # Font file types
 def extract_text_from_html(file_path):
    """Extract text content from a single HTML file."""
    with open(file_path, "r", encoding="utf-8") as f:
        soup = BeautifulSoup(f.read(), "html.parser")
        return soup.get_text()
 def get_used_characters(files):
    """Collect unique characters from all .html files in the given directory."""
    char_set = set()
    for file in files:
        text = extract_text_from_html(file)
        char_set.update(text)
    return "".join(sorted(char_set))
 def find_font_files(directory):
    """Find all font files in the given directory, recursively."""
    font_files = []
    for root, _, files in os.walk(directory):
        for file in files:
            if file.endswith(FONT_EXTENSIONS):
                font_files.append(os.path.join(root, file))
    return font_files
 def subset_font_in_place(font_path, characters):
    """Subsets the given font file to include only the specified characters."""
    # Convert characters to their integer code points
    unicode_set = {ord(c) for c in characters}
    font = TTFont(font_path)
    options = Options()
    options.drop_tables += ["DSIG"]
    options.drop_tables += ["LTSH", "VDMX", "hdmx", "gasp"]
    options.unicodes = unicode_set
    options.variations = False
    options.drop_variations = True
    options.layout_features = ["*"]  # keep all OT features
    options.hinting = False
    # Preserve original format if it was WOFF/WOFF2
    if font_path.endswith(".woff2"):
        options.flavor = "woff2"
    elif font_path.endswith(".woff"):
        options.flavor = "woff"
    subsetter = Subsetter(options)
    subsetter.populate(unicodes=unicode_set)
    subsetter.subset(font)
    # Overwrite the original font file
    font.save(font_path)
    print(f"Subsetted font in place: {font_path}")
 if __name__ == "__main__":
    used_chars = get_used_characters(sys.argv[2:])
    print(f"Extracted {len(used_chars)} unique characters from {len(sys.argv[2:])} HTML files.")
    font_files = find_font_files(sys.argv[1])
    print(f"Found {len(font_files)} font files to subset.")
    for font_file in font_files:
        subset_font_in_place(font_file, used_chars)
--- a/config.toml
+++ b/config.toml
@@ -1,7 +1,5 @@
 baseURL = "https://danilafe.com"
 theme = "vanilla"
 pygmentsCodeFences = true
 pygmentsUseClasses = true
 summaryLength = 20
 defaultContentLanguage = 'en'
@@ -22,6 +20,9 @@ defaultContentLanguage = 'en'
  home = ["html","rss","toml"]
 [markup]
  [markup.highlight]
    codeFences = true
    noClasses = false
  [markup.tableOfContents]
    endLevel = 4
    ordered = false
--- a/content/blog/00_spa_agda_intro.md
+++ b/content/blog/00_spa_agda_intro.md
@@ -106,4 +106,5 @@ Here are the posts that I’ve written so far for this series:
 * {{< draftlink "Our Programming Language" "05_spa_agda_semantics" >}}
 * {{< draftlink "Control Flow Graphs" "06_spa_agda_cfg" >}}
 * {{< draftlink "Connecting Semantics and Control Flow Graphs" "07_spa_agda_semantics_and_cfg" >}}
-* {{< draftlink "A Verified Forward Analysis" "08_spa_forward" >}}
+* {{< draftlink "Forward Analysis" "08_spa_agda_forward" >}}
 * {{< draftlink "Verifying the Forward Analysis" "09_spa_agda_verified_forward" >}}
--- a/content/blog/01_spa_agda_lattices.md
+++ b/content/blog/01_spa_agda_lattices.md
@@ -79,6 +79,7 @@ a less specific output! The more you know going in, the more you should know
 coming out. Similarly, when given less specific / vaguer information, the
 analysis shouldn't produce a more specific answer -- how could it do that?
 This leads us to come up with the following rule:
 {#define-monotonicity}
 {{< latex >}}
 \textbf{if}\ \text{input}_1 \le \text{input}_2,
--- a/content/blog/02_types_variables.md
+++ b/content/blog/02_types_variables.md
@@ -339,9 +339,8 @@ this means the rule applies to (object) variables declared to have type
 our system. A single rule takes care of figuring the types of _all_
 variables.
-{{< todo >}}
+> [!TODO]
-The rest of this, but mostly statements.
+> The rest of this, but mostly statements.
 {{< /todo >}}
 ### This Page at a Glance
 #### Metavariables
--- a/content/blog/04_spa_agda_fixedpoint.md
+++ b/content/blog/04_spa_agda_fixedpoint.md
@@ -55,6 +55,7 @@ Now, let's start with the least element of our lattice, denoted \(\bot\).
 A lattice of finite height is guaranteed to have such an element. If it didn't,
 we could always extend chains by tacking on a smaller element to their bottom,
 and then the lattice wouldn't have a finite height anymore.
 {#start-least}
 Now, apply \(f\) to \(\bot\) to get \(f(\bot)\). Since \(\bot\) is the least
 element, it must be true that \(\bot \le f(\bot)\). Now, if it's "less than or equal",
--- a/content/blog/05_spa_agda_semantics/index.md
+++ b/content/blog/05_spa_agda_semantics/index.md
@@ -262,6 +262,7 @@ expressions, and the letter \(v\) to stand for values. Finally, we'll write
 \(\rho, e \Downarrow v\) to say that "in an environment \(\rho\), expression \(e\)
 evaluates to value \(v\)". Our two previous examples of evaluating `x+1` can
 thus be written as follows:
 {#notation-for-environments}
 {{< latex >}}
 \{ \texttt{x} \mapsto 42 \}, \texttt{x}+1 \Downarrow 43 \\
--- a/content/blog/06_spa_agda_cfg/index.md
+++ b/content/blog/06_spa_agda_cfg/index.md
@@ -130,7 +130,7 @@ by one, leading to another `suc n` in the final type. This makes sense because i
 Here's my definition of `Graph`s written using `Fin`:
-{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 24 39 >}}
+{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 23 38 >}}
 I explicitly used a `size` field, which determines how many nodes are in the
 graph, and serves as the upper bound for the edge indices. From there, an
@@ -176,7 +176,7 @@ we will connect each of the outputs of one to each of the inputs of the other.
 This is defined by the operation `g₁ ↦ g₂`, which sequences two graphs `g₁` and `g₂`:
-{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 72 83 >}}
+{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 71 82 >}}
 The definition starts out pretty innocuous, but gets a bit complicated by the
 end. The sum of the numbers of nodes in the two operands becomes the new graph
@@ -238,7 +238,7 @@ operation when combining the sub-CFGs of the "if" and "else" branches of an
 `if`/`else`, which both follow the condition, and both proceed to the code after
 the conditional.
-{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 59 70 >}}
+{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 58 69 >}}
 Everything here is just concatenation; we pool together the nodes, edges,
 inputs, and outputs, and the main source of complexity is the re-indexing.
@@ -250,12 +250,12 @@ from the graph for `while` loops I showed above; the reason for that is that
 I currently don't include the conditional expressions in my CFG. This is a
 limitation that I will address in future work.
-{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 85 95 >}}
+{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 84 94 >}}
 Given these thee operations, I construct Control Flow Graphs as follows, where
 `singleton` creates a new CFG node with the given list of simple statements:
-{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 122 126 >}}
+{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 121 125 >}}
 Throughout this, I've been liberal to include empty CFG nodes as was convenient.
 This is a departure from the formal definition I gave above, but it makes
--- a/content/blog/08_spa_agda_forward/index.md
+++ b/content/blog/08_spa_agda_forward/index.md
@@ -0,0 +1,445 @@
 ---
 title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 8: Forward Analysis"
 series: "Static Program Analysis in Agda"
 description: "In this post, I use the monotone lattice framework and verified CFGs to define a sign analysis"
 date: 2024-12-01T15:09:07-08:00
 tags: ["Agda", "Programming Languages"]
 ---
 In the previous post, I showed that the Control Flow graphs we built of our
 programs match how they are really executed. This means that we can rely
 on these graphs to compute program information. In this post, we finally
 get to compute that information. Here's a quick bit paraphrasing from last time
 that provides a summary of our approach:
 1. We will construct a finite-height lattice. Every single element of this
   lattice will contain information about each variable at each node in the
   Control Flow Graph.
 2. We will then define a monotonic function that update this information using
   the structure encoded in the CFG’s edges and nodes.
 3. Then, using the fixed-point algorithm, we will find the least element of the
   lattice, which will give us a precise description of all program variables at
   all points in the program.
 4. Because we have just validated our CFGs to be faithful to the language’s
   semantics, we’ll be able to prove that our algorithm produces accurate results.
 Let's jump right into it!
 ### Choosing a Lattice
 A lot of this time, we have been [talking about lattices]({{< relref "01_spa_agda_lattices" >}}),
 particularly [lattices of finite height]({{< relref "03_spa_agda_fixed_height" >}}).
 These structures represent things we know about the program, and provide operators
 like \((\sqcup)\) and \((\sqcap)\) that help us combine such knowledge.
 The forward analysis code I present here will work with any finite-height
 lattice, with the additional constraint that equivalence of lattices
 is decidable, which comes from [the implementation of the fixed-point algorithm]({{< relref "04_spa_agda_fixedpoint" >}}),
 in which we routinely check if a function's output is the same as its input.
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 4 8 >}}
 The finite-height lattice `L` is intended to describe the state of a single
 variable.
 One example of a lattice that can be used as `L` is our
 sign lattice. We've been using the sign lattice in our examples [from the very beginning]({{< relref "01_spa_agda_lattices#lattices" >}}),
 and we will stick with it for the purposes of this explanation. However, this
 lattice alone does not describe our program, since it only talks about a single
 sign; programs have lots of variables, all of which can have different signs!
 So, we might go one step further and define a map lattice from variables to
 their signs:
 {{< latex >}}
 \text{Variable} \to \text{Sign}
 {{< /latex >}}
 We [have seen]({{< relref "02_spa_agda_combining_lattices#the-map-lattice" >}})
 that we can turn any lattice \(L\) into a map lattice \(A \to L\), for any
 type of keys \(A\). In this case, we will define \(A \triangleq \text{Variable}\),
 and \(L \triangleq \text{Sign}\). The
 [sign lattice has a finite height]({{< relref "02_spa_agda_combining_lattices#the-map-lattice" >}}),
 and I've proven that, as long as we pick a finite set of keys, [map lattices
 \(A \to L\) have a finite height if \(L\) has a finite height]({{< relref "03_spa_agda_fixed_height#fixed-height-of-the-map-lattice" >}}).
 Since a program's text is finite, \(\text{Variable}\) is a finite set, and
 we have ourselves a finite-height lattice \(\text{Variable} \to \text{Sign}\).
 We're on the right track, but even the lattice we have so far is not sufficient.
 That's because variables have different signs at different points in the program!
 You might initialize a variable with `x = 1`, making it positive, and then
 go on to compute some arbitrary function using loops and conditionals. For
 each variable, we need to keep track of its sign at various points in the code.
 When we [defined Control Flow Graphs]({{< relref "06_spa_agda_cfg" >}}), we
 split our programs into sequences of statements that are guaranteed to execute
 together --- basic blocks. For our analysis, we'll keep per-variable for
 each basic block in the program. Since basic blocks are nodes in the Control Flow
 Graph of our program, our whole lattice will be as follows:
 {#whole-lattice}
 {{< latex >}}
 \text{Info} \triangleq \text{NodeId} \to (\text{Variable} \to \text{Sign})
 {{< /latex >}}
 We follow the same logic we just did for the variable-sign lattice; since
 \(\text{Variable} \to \text{Sign}\) is a lattice of finite height, and since
 \(\text{NodeId}\) is a finite set, the whole \(\text{Info}\) map will be
 a lattice with a finite height.
 Notice that both the sets of \(\text{Variable}\) and \(\text{NodeId}\) depend
 on the program in question. The lattice we use is slightly different for
 each input program! We can use Agda's parameterized modules to automaitcally
 parameterize all our functions over programs:
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 36 37 >}}
 Now, let's make the informal descriptions above into code, by instantiating
 our map lattice modules. First, I invoked the code for the smaller variable-sign
 lattice. This ended up being quite long, so that I could rename variables I
 brought into scope. I will collapse the relevant code block; suffice to say
 that I used the suffix `v` (e.g., renaming `_⊔_` to `_⊔ᵛ_`) for properties
 and operators to do with variable-sign maps (in Agda: `VariableValuesFiniteMap`).
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 41 82 "" "**(Click here to expand the module uses for variable-sign maps)**" >}}
 I then used this lattice as an argument to the map module again, to
 construct the top-level \(\text{Info}\) lattice (in Agda: `StateVariablesFiniteMap`).
 This also required a fair bit of code, most of it to do with renaming.
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 85 112 "" "**(Click here to expand the module uses for the top-level lattice)**" >}}
 ### Constructing a Monotone Function
 We now have a lattice in hand; the next step is to define a function over
 this lattice. For us to be able to use the fixed-point algorithm on this
 function, it will need to be [monotonic]({{< relref "01_spa_agda_lattices#define-monotonicity" >}}).
 Our goal with static analysis is to compute information about our program; that's
 what we want the function to do. When the lattice we're using is the sign lattice,
 we're trying to determine the signs of each of the variables in various parts
 of the program. How do we go about this?
 Each piece of code in the program might change a variable's sign. For instance,
 if `x` has sign \(0\), and we run the statement `x = x - 1`, the sign of
 `x` will be \(-\). If we have an expression `y + z`, we can use the signs of
 `y` and `z` to compute the sign of the whole thing. This is a form
 of [abstract interpretation](https://en.wikipedia.org/wiki/Abstract_interpretation),
 in which we almost-run the program, but forget some details (e.g., the
 exact values of `x`, `y`, and `z`, leaving only their signs). The exact details
 of how this partial evaluation is done are analysis-specific; in general, we
 simply require an analysis to provide an evaluator. We will define
 [an evaluator for the sign lattice below](#instantiating-with-the-sign-lattice).
 {#general-evaluator}
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 166 167 >}}
 From this, we know how each statement and basic block will change variables
 in the function. But we have described them process as "if a variable has
 sign X, it becomes sign Y" -- how do we know what sign a variable has _before_
 the code runs? Fortunately, the Control Flow Graph tells us exactly
 what code could be executed before any given basic block. Recall that edges
 in the graph describe all possible jumps that could occur; thus, for any
 node, the incoming edges describe all possible blocks that can precede it.
 This is why we spent all that time [defining the `predecessors` function]({{< relref "06_spa_agda_cfg#additional-functions" >}}).
 We proceed as follows: for any given node, find its predecessors. By accessing
 our \(\text{Info}\) map for each predecessor, we can determine our current
 best guess of variable signs at that point, in the form of a \(\text{Variable} \to \text{Sign}\)
 map (more generally, \(\text{Variable} \to L\) map in an arbitrary analysis).
 We know that any of these predecessors could've been the previous point of
 execution; if a variable `x` has sign \(+\) in one predecessor and \(-\)
 in another, it can be either one or the other when we start executing the
 current block. Early on, we saw that [the \((\sqcup)\) operator models disjunction
 ("A or B")]({{< relref "01_spa_agda_lattices#lub-glub-or-and" >}}). So, we apply
 \((\sqcup)\) to the variable-sign maps of all predecessors. The
 [reference _Static Program Analysis_ text](https://cs.au.dk/~amoeller/spa/)
 calls this operation \(\text{JOIN}\):
 {#join-preds}
 {{< latex >}}
 \textit{JOIN}(v) = \bigsqcup_{w \in \textit{pred}(v)} \llbracket w \rrbracket
 {{< /latex >}}
 The Agda implementation uses a `foldr`:
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 139 140 >}}
 Computing the "combined incoming states" for any node is a monotonic function.
 This follows from the monotonicity of \((\sqcup)\) --- in both arguments ---
 and the definition of `foldr`.
 {{< codelines "agda" "agda-spa/Lattice.agda" 143 151 "" "**(Click here to expand the general proof)**" >}}
 From this, we can formally state that \(\text{JOIN}\) is monotonic. Note that
 the input and output lattices are different: the input lattice is the lattice
 of variable states at each block, and the output lattice is a single variable-sign
 map, representing the combined preceding state at a given node.
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 145 149 >}}
 Above, the `m₁≼m₂⇒m₁[ks]≼m₂[ks]` lemma states that for two maps with the same
 keys, where one map is less than another, all the values for any subset of keys
 `ks` are pairwise less than each other (i.e. `m₁[k]≼m₂[k]`, and `m₁[l]≼m₂[l]`, etc.).
 This follows from the definition of "less than" for maps.
 {#less-than-lemma}
 So those are the two pieces: first, join all the preceding states, then use
 the abstract interpretation function. I opted to do both of these in bulk:
 1. Take an initial \(\text{Info}\) map, and update every basic block's entry
   to be the join of its predecessors.
 2. In the new joined map, each key now contains the variable state at
   the beginning of the block; so, apply the abstract interpretation function
   via `eval` to each key, computing the state at the end of the block.
 I chose to do these in bulk because this way, after each application of
 the function, we have updated each block with exactly one round of information.
 The alternative --- which is specified in the reference text --- is to update
 one key at a time. The difference there is that updates to later keys might be
 "tainted" by updates to keys that came before them. This is probably fine
 (and perhaps more efficient, in that it "moves faster"), but it's harder to
 reason about.
 #### Generalized Update
 To implement bulk assignment, I needed to implement the source text's
 Exercise 4.26:
 > __Exercise 4.26__: Recall that \(f[a \leftarrow x]\) denotes the function that is identical to
 > \(f\) except that it maps \(a\) to \(x\). Assume \(f : L_1 \to (A \to L_2)\)
 > and \(g : L_1 \to L_2\) are monotone functions where \(L_1\) and \(L_2\) are
 > lattices and \(A\) is a set, and let \(a \in A\). (Note that the codomain of
 > \(f\) is a map lattice.)
 >
 > Show that the function \(h : L_1 \to (A \to L_2)\)
 > defined by \(h(x) = f(x)[a \leftarrow g(x)]\) is monotone.
 In fact, I generalized this statement to update several keys at once, as follows:
 {{< latex >}}
 h(x) = f(x)[a_1 \leftarrow g(a_1, x),\ ...,\ a_n \leftarrow g(a_n, x)]
 {{< /latex >}}
 I called this operation "generalized update".
 At first, the exercise may not obviously correspond to the bulk operation
 I've described. Particularly confusing is the fact that it has two lattices,
 \(L_1\) and \(L_2\). In fact, the exercise results in a very general theorem;
 we can exploit a more concrete version of the theorem by setting
 \(L_1 \triangleq A \to L_2\), resulting in an overall signature for \(f\) and \(h\):
 {{< latex >}}
 f : (A \to L_2) \to (A \to L_2)
 {{< /latex >}}
 In other words, if we give the entire operation in Exercise 4.26 a type,
 it would look like this:
 {{< latex >}}
 \text{ex}_{4.26} : \underbrace{K}_{\text{value of}\ a} \to \underbrace{(\text{Map} \to V)}_{\text{updater}} \to \underbrace{\text{Map} \to \text{Map}}_{f} \to \underbrace{\text{Map} \to \text{Map}}_{h}
 {{< /latex >}}
 That's still more general than we need it. This here allows us to modify
 any map-to-map function by updating a certain key in that function. If we
 _just_ want to update keys (as we do for the purposes of static analysis),
 we can recover a simpler version by setting \(f \triangleq id\), which
 results in an updater \(h(x) = x[a \leftarrow g(x)]\), and a signature for
 the exercise:
 {{< latex >}}
 \text{ex}_{4.26} : \underbrace{K}_{\text{value of}\ a} \to \underbrace{(\text{Map} \to V)}_{\text{updater}\ g} \to \underbrace{\text{Map}}_{\text{old map}} \to \underbrace{\text{Map}}_{\text{updated map}}
 {{< /latex >}}
 This looks just like Haskell's [`Data.Map.adjust` function](https://hackage.haskell.org/package/containers-0.4.0.0/docs/src/Data-Map.html#adjust), except that it
 can take the entire map into consideration when updating a key.
 My generalized version takes in a list of keys to update, and makes the updater
 accept a key so that its behavior can be specialized for each entry it changes.
 The sketch of the implementation is in the `_updating_via_` function from
 the `Map` module, and its helper `transform`. Here, I collapse its definition,
 since it's not particularly important.
 {{< codelines "agda" "agda-spa/Lattice/Map.agda" 926 931 "" "**(Click here to see the definition of `transform`)**" >}}
 The proof of monotonicity --- which is the solution to the exercise --- is
 actually quite complicated. I will omit its description, and show it here
 in another collapsed block.
 {{< codelines "agda" "agda-spa/Lattice/Map.agda" 1042 1105 "" "**(Click here to see the proof of monotonicity of \(h\))**" >}}
 Given a proof of the exercise, all that's left is to instantiate the theorem
 with the argument I described. Specifically:
 * \(L_1 \triangleq \text{Info} \triangleq \text{NodeId} \to (\text{Variable} \to \text{Sign})\)
 * \(L_2 \triangleq \text{Variable} \to \text{Sign} \)
 * \(A \triangleq \text{NodeId}\)
 * \(f \triangleq \text{id} \triangleq x \mapsto x\)
 * \(g(k, m) = \text{JOIN}(k, m)\)
 In the equation for \(g\), I explicitly insert the map \(m\) instead of leaving
 it implicit as the textbook does. In Agda, this instantiation for joining
 all predecessor looks like this (using `states` as the list of keys to update,
 indicating that we should update _every_ key):
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 152 157 >}}
 And the one for evaluating all programs looks like this:
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 215 220 >}}
 Actually, we haven't yet seen that `updateVariablesFromStmt`. This is
 a function that we can define using the user-provided abtract interpretation
 `eval`. Specifically, it handles the job of updating the sign of a variable
 once it has been assigned to (or doing nothing if the statement is a no-op).
 {#define-updateVariablesFromStmt}
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 191 193 >}}
 The `updateVariablesFromExpression` is now new, and it is yet another map update,
 which changes the sign of a variable `k` to be the one we get from running
 `eval` on it. Map updates are instances of the generalized update; this
 time, the updater \(g\) is `eval`. The exercise requires the updater to be
 monotonic, which constrains the user-provided evaluation function to be
 monotonic too.
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 173 181 >}}
 We finally write the `analyze` function as the composition of the two bulk updates:
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 226 232 >}}
 ### Instantiating with the Sign Lattice
 Thus far, I've been talking about the sign lattice throughout, but implementing
 the Agda code in terms of a general lattice `L` and evaluation function `eval`.
 In order to actually run the Agda code, we do need to provide an `eval` function,
 which implements the logic we used above, in which a zero-sign variable \(x\)
 minus one was determined to be negative. For binary operators specifically,
 I've used the table provided in the textbook; here they are:
 {{< figure src="plusminus.png" caption="Cayley tables for abstract interpretation of plus and minus" >}}
 These are pretty much common sense:
 * A positive plus a positive is still positive, so \(+\ \hat{+}\ + = +\)
 * A positive plus any sign could be any sign still, so \(+\ \hat{+}\ \top = \top\)
 * Any sign plus "impossible" is impossible, so \(\top\ \hat{+} \bot = \bot\).
 * etc.
 The Agda encoding for the plus function is as follows, and the one for minus
 is similar.
 {{< codelines "agda" "agda-spa/Analysis/Sign.agda" 76 94 >}}
 As the comment in the block says, it would be incredibly tedious to verify
 the monotonicity of these tables, since you would have to consider roughly
 125 cases _per argument_: for each (fixed) sign \(s\) and two other signs
 \(s_1 \le s_2\), we'd need to show that \(s\ \hat{+}\ s_1 \le s\ \hat{+}\ s_2\).
 I therefore commit the _faux pas_ of using `postulate`. Fortunately, the proof
 of monotonicity is not used for the execution of the program, so we will
 get away with this, barring any meddling kids.
 From this, all that's left is to show that for any expression `e`, the
 evaluation function:
 {{< latex >}}
 \text{eval} : \text{Expr} \to (\text{Variable} \to \text{Sign}) \to \text{Sign}
 {{< /latex >}}
 is monotonic. It's defined straightforwardly and very much like an evaluator /
 interpreter, suggesting that "abstract interpretation" is the correct term here.
 {{< codelines "agda" "agda-spa/Analysis/Sign.agda" 176 184 >}}
 Thought it won't happen, it was easier to just handle the case where there's
 an undefined variable; I give it "any sign". Otherwise, the function simply
 consults the sign tables for `+` or `-`, as well as the known signs of the
 variables. For natural number literals, it assigns `0` the "zero" sign, and
 any other natural number the "\(+\)".
 To prove monotonicity, we need to consider two variable maps (one less than
 the other), and show that the abstract interpretation respects that ordering.
 This boils down to the fact that the `plus` and `minus` tables are monotonic
 in both arguments (thus, if their sub-expressions are evaluated monotonically
 given an environment, then so is the whole addition or subtraction), and
 to the fact that for two maps `m₁ ≼ m₂`, the values at corresponding keys
 are similarly ordered: `m₁[k] ≼ m₂[k]`. We [saw that above](#less-than-lemma).
 {{< codelines "agda" "agda-spa/Analysis/Sign.agda" 186 223 "" "**(Click to expand the proof that the evaluation function for signs is monotonic)**" >}}
 That's all we need. With this, I just instantiate the `Forward` module we have
 been working with, and make use of the `result`. I also used a `show`
 function (which I defined) to stringify that output.
 {{< codelines "agda" "agda-spa/Analysis/Sign.agda" 225 229 >}}
 But wait, `result`? We haven't seen a result just yet. That's the last piece,
 and it involves finally making use of the fixed-point algorithm.
 ### Invoking the Fixed Point Algorithm
 Our \(\text{Info}\) lattice is of finite height, and the function we have defined
 is monotonic (by virtue of being constructed only from map updates, which
 are monotonic by Exercise 4.26, and from function composition, which preserves
 monotonicity). We can therefore apply the fixed-point-algorithm, and compute
 the least fixed point:
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 235 238 >}}
 With this, `analyze` is the result of our forward analysis!
 In a `Main.agda` file, I invoked this analysis on a sample program:
 ```Agda
 testCode : Stmt
 testCode =
    ⟨ "zero" ← (# 0) ⟩ then
    ⟨ "pos" ← ((` "zero") Expr.+ (# 1)) ⟩ then
    ⟨ "neg" ← ((` "zero") Expr.- (# 1)) ⟩ then
    ⟨ "unknown" ← ((` "pos") Expr.+ (` "neg")) ⟩
 testProgram : Program
 testProgram = record
    { rootStmt = testCode
    }
 open WithProg testProgram using (output; analyze-correct)
 main = run {0ℓ} (putStrLn output)
 ```
 The result is verbose, since it shows variable signs for each statement
 in the program. However, the key is the last basic block, which shows
 the variables at the end of the program. It reads:
 ```
 {"neg" ↦ -, "pos" ↦ +, "unknown" ↦ ⊤, "zero" ↦ 0, }
 ```
 ### Verifying the Analysis
 We now have a general framework for running forward analyses: you provide
 an abstract interpretation function for expressions, as well as a proof
 that this function is monotonic, and you get an Agda function that takes
 a program and tells you the variable states at every point. If your abstract
 interpretation function is for determining the signs of expressions, the
 final result is an analysis that determines all possible signs for all variables,
 anywhere in the code. It's pretty easy to instantiate this framework with
 another type of forward analysis --- in fact, by switching the
 `plus` function to one that uses `AboveBelow ℤ`, rather than `AboveBelow Sign`:
 ```Agda
 plus : ConstLattice → ConstLattice → ConstLattice
 plus ⊥ᶜ _ = ⊥ᶜ
 plus _ ⊥ᶜ = ⊥ᶜ
 plus ⊤ᶜ _ = ⊤ᶜ
 plus _ ⊤ᶜ = ⊤ᶜ
 plus [ z₁ ]ᶜ [ z₂ ]ᶜ = [ z₁ Int.+ z₂ ]ᶜ
 ```
 we can defined a constant-propagation analysis.
 ```
 {"neg" ↦ -1, "pos" ↦ 1, "unknown" ↦ 0, "zero" ↦ 0, }
 ```
 However, we haven't proved our analysis correct, and we haven't yet made use of
 the CFG-semantics equivalence that we
 [proved in the previous section]({{< relref "07_spa_agda_semantics_and_cfg" >}}).
 I was hoping to get to it in this post, but there was just too much to
 cover. So, I will get to that in the next post, where we will make use
 of the remaining machinery to demonstrate that the output of our analyzer
 matches reality.
--- a/content/blog/08_spa_agda_forward/plusminus.png
+++ b/content/blog/08_spa_agda_forward/plusminus.png
--- a/content/blog/08_spa_agda_forward/thumbnail.png
+++ b/content/blog/08_spa_agda_forward/thumbnail.png
--- a/content/blog/09_spa_agda_verified_forward/index.md
+++ b/content/blog/09_spa_agda_verified_forward/index.md
@@ -0,0 +1,547 @@
 ---
 title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 9: Verifying the Forward Analysis"
 series: "Static Program Analysis in Agda"
 description: "In this post, I prove that the sign analysis from the previous is correct"
 date: 2024-12-25T19:00:00-08:00
 tags: ["Agda", "Programming Languages"]
 left_align_code: true
 ---
 In the previous post, we put together a number of powerful pieces of machinery
 to construct a sign analysis. However, we still haven't verified that this
 analysis produces correct results. For the most part, we already have the
 tools required to demonstrate correctness; the most important one
 is the [validity of our CFGs]({{< relref "07_spa_agda_semantics_and_cfg" >}})
 relative to [the semantics of the little language]({{< relref "05_spa_agda_semantics" >}}).
 ### High-Level Algorithm
 We'll keep working with the sign lattice as an example, keeping in mind
 how what we do generalizes to a any lattice \(L\) describing a variable's
 state. The general shape of our argument will be as follows, where I've underlined and
 numbered assumptions or aspects that we have yet to provide.
 1. Our fixed-point analysis from the previous section gave us a result \(r\)
   that satisfies the following equation:
   {{< latex >}}
   r = \text{update}(\text{join}(r))
   {{< /latex >}}
   Above \(\text{join}\) applies the [predecessor-combining function]({{< relref "08_spa_agda_forward#join-preds" >}})
   from the previous post to each state (corresponding to `joinAll` in Agda)
   and \(\text{update}\) performs one round of abstract interpretation.
 2. Because of the [correspondence of our semantics and CFGs]({{< relref "07_spa_agda_semantics_and_cfg" >}}),
   each program evaluation in the form \(\rho, s \Rightarrow \rho'\)
   corresponds to a path through the Control Flow Graph. Along the path,
   each node contains simple statements, which correspond to intermediate steps
   in evaluating the program. These will also be in the form
   \(\rho_1, b \Rightarrow \rho_2\).
 3. We will proceed iteratively, stepping through the trace one basic block at
   a time. At each node in the graph:
   * We will assume that the beginning state (the variables in \(\rho_1\)) are
     {{< internal "correctly-described" >}}
     correctly described
     {{< /internal >}}
     by one of the predecessors of the current node. Since
     {{< internal "disjunction" >}}
     joining represents "or"
     {{< /internal >}},
     that is the same
     as saying that \(\text{join}(r)\)
     contains an accurate description of \(\rho_1\).
   * Because
     {{< internal "abstract-interpretation" >}}
     the abstract interpretation function preserves accurate descriptions
     {{< /internal >}},
     if \(\text{join}(r)\) contains an accurate description \(\rho_1\), then applying our
     abstract interpretation function via \(\text{update}\) should result in
     a map that contains an accurate-described \(\rho_2\). In other words, \(\text{update}(\text{join}(r))\)
     describes \(\rho_2\) at the current block.
     {{< internal "equivalence" >}}
     By the equation above
     {{< /internal >}}, that's the same as saying
     \(r\) describes \(\rho_2\) at the current block.
   * Since the trace is a path through a graph, there must be an edge from
     the current basic block to the next. This means that the current basic
     block is a predecessor of the next one. From the previous point, we know
     that \(\rho_2\) is accurately described by this predecessor, fulfilling
     our earlier assumption and allowing us to continue iteration.
 So, what are the missing pieces?
 1. We need to define what it means for a lattice (like our sign lattice)
   to "correctly describe" what happens when evaluating a program for real.
   For example, the \(+\) in sign analysis describes values that are bigger than zero,
   and a map like `{x:+}` states that `x` can only take on positive values.
 2. We've seen before [the \((\sqcup)\) operator models disjunction
   ("A or B")]({{< relref "01_spa_agda_lattices#lub-glub-or-and" >}}), but
   that was only an informal observation; we'll need to specify it preceisely.
 3. Each analysis [provides an abstract interpretation `eval` function]({{< relref "08_spa_agda_forward#general-evaluator" >}}).
   However, until now, nothing has formally constrained this function; we could
   return \(+\) in every case, even though that would not be accurate. We will
   need, for each analysis, a proof that its `eval` preserves accurate descriptions.
 4. The equalities between our lattice elements [are actually equivalences]({{< relref "01_spa_agda_lattices#definitional-equality" >}}),
   which helps us use simpler representations of data structures. Thus, even
   in statements of the fixed point algorithm, our final result is a value \(a\)
   such that \(a \approx f(a)\). We need to prove that our notion of equivalent
   lattice elements plays nicely with correctness.
 Let's start with the first bullet point.
 ### A Formal Definition of Correctness
 When a variable is mapped to a particular sign (like `{ "x": + }`),
 what that really says is that the value of `x` is greater than zero. Recalling
 from [the post about our language's semantics]({{< relref "05_spa_agda_semantics#notation-for-environments" >}})
 that we use the symbol \(\rho\) to represent mappings of variables to
 their values, we might write this claim as:
 {{< latex >}}
 \rho(\texttt{x}) > 0
 {{< /latex >}}
 This is a good start, but it's a little awkward defining the meaning of "plus"
 by referring to the context in which it's used (the `{ "x": ... }` portion
 of the expression above). Instead, let's associate with each sign (like \(+\)) a
 predicate: a function that takes a value, and makes a claim about that value
 ("this is positive"):
 {{< latex >}}
 \llbracket + \rrbracket\ v = v > 0
 {{< /latex >}}
 The notation above is a little weird unless you, like me, have a background in
 Programming Language Theory (❤️). This comes from [denotational semantics](https://en.wikipedia.org/wiki/Denotational_semantics);
 generally, one writes:
 {{< latex >}}
 \llbracket \text{thing} \rrbracket = \text{the meaning of the thing}
 {{< /latex >}}
 Where \(\llbracket \cdot \rrbracket\) is really a function (we call it
 the _semantic function_) that maps things to
 their meaning. Then, the above equation is similar to the more familiar
 \(f(x) = x+1\): function and arguments on the left, definition on the right. When
 the "meaning of the thing" is itself a function, we could write it explicitly
 using lambda-notation:
 {{< latex >}}
 \llbracket \text{thing} \rrbracket = \lambda x.\ \text{body of the function}
 {{< /latex >}}
 Or, we could use the Haskell style and write the new variable on the left of
 the equality:
 {{< latex >}}
 \llbracket \text{thing} \rrbracket\ x = \text{body of the function}
 {{< /latex >}}
 That is precisely what I'm doing above with \(\llbracket + \rrbracket\).
 With this in mind, we could define the entire semantic function for the
 sign lattice as follows:
 {{< latex >}}
 \llbracket + \rrbracket\ v = v\ \texttt{>}\ 0 \\
 \llbracket 0 \rrbracket\ v = v\ \texttt{=}\ 0 \\
 \llbracket - \rrbracket\ v = v\ \texttt{<}\ 0 \\
 \llbracket \top \rrbracket\ v = \text{true} \\
 \llbracket \bot \rrbracket\ v = \text{false}
 {{< /latex >}}
 In Agda, the integer type already distinguishes between "negative natural" or
 "positive natural" cases, which made it possible to define the semantic function
 {{< sidenote "right" "without-note" "without using inequalities." >}}
 Reasoning about inequalities is painful, sometimes requiring a number of
 lemmas to arrive at a result that is intuitively obvious. Coq has a powerful
 tactic called <a href="https://coq.inria.fr/doc/v8.11/refman/addendum/micromega.html#coq:tacn.lia"><code>lia</code></a>
 that automatically solves systems of inequalities, and I use it liberally.
 However, lacking such a tactic in Agda, I would like to avoid inequalities
 if they are not needed.
 {{< /sidenote >}}
 {{< codelines "agda" "agda-spa/Analysis/Sign.agda" 114 119 >}}
 Notably, \(\llbracket \top \rrbracket\ v\) always holds, and
 \(\llbracket \bot \rrbracket\ v\) never does. __In general__, we will always
 need to define a semantic function for whatever lattice we are choosing for
 our analysis.
 It's important to remember from the previous post that the sign lattice
 (or, more generally, our lattice \(L\)) is only a component of the
 [lattice we use to instantiate the analysis]({{< relref "08_spa_agda_forward#whole-lattice" >}}).
 We at least need to define what it means for the \(\text{Variable} \to \text{Sign}\)
 portion of that lattice to be correct. This way, we'll have correctness
 criteria for each key (CFG node) in the top-level \(\text{Info}\) lattice.
 Since a map from variables to their sign characterizes not a single value \(v\)
 but a whole environment \(\rho\), something like this is a good start:
 {{< latex >}}
 \llbracket \texttt{\{} x_1: s_1, ..., x_n: s_n \texttt{\}} \rrbracket\ \rho = \llbracket s_1 \rrbracket\ \rho(x_1)\ \text{and}\ ...\ \text{and}\ \llbracket s_n \rrbracket\ \rho(x_n)
 {{< /latex >}}
 As a concrete example, we might get:
 {{< latex >}}
 \llbracket \texttt{\{} \texttt{x}: +, \texttt{y}: - \texttt{\}} \rrbracket\ \rho = \rho(\texttt{x})\ \texttt{>}\ 0\ \text{and}\ \rho(\texttt{y})\ \texttt{<}\ 0
 {{< /latex >}}
 This is pretty good, but not quite right. For instance, the initial state of
 the program --- before running the analysis --- assigns \(\bot\) to each
 element. This is true because our fixed-point algorithm [starts with the least
 element of the lattice]({{< relref "04_spa_agda_fixedpoint#start-least" >}}).
 But even for a single-variable map `{x: ⊥ }`, the semantic function above would
 give:
 {{< latex >}}
 \llbracket \texttt{\{} \texttt{x}: \bot \texttt{\}} \rrbracket\ \rho = \text{false}
 {{< /latex >}}
 That's clearly not right: our initial state should be possible, lest
 the entire proof be just a convoluted [_ex falso_](https://en.wikipedia.org/wiki/Principle_of_explosion)!
 There is another tricky aspect of our analysis, which is primarily defined
 [using the join (\(\sqcup\)) operator]({{< relref "08_spa_agda_forward#join-preds" >}}).
 Observe the following example:
 ```C
 // initial state: { x: ⊥ }
 if b {
  x = 1; // state: { x: + }
 } else {
  // state unchanged: { x: ⊥ }
 }
 // state: { x: + } ⊔ { x: ⊥ } = { x: + }
 ```
 Notice that in the final state, the sign of `x` is `+`, even though when
 `b` is `false`, the variable is never set. In a simple language like ours,
 without variable declaration points, this is probably the best we could hope
 for. The crucial observation, though, is that the oddness only comes into
 play with variables that are not set. In the "initial state" case, none
 of the variables have been modified; in the `else` case of the conditional,
 `x` was never assigned to. We can thus relax our condition to an if-then:
 if a variable is in our environment \(\rho\), then the variable-sign lattice's
 interpretation accurately describes it.
 {{< latex >}}
 \begin{array}{ccc}
 \llbracket \texttt{\{} x_1: s_1, ..., x_n: s_n \texttt{\}} \rrbracket\ \rho & = & & \textbf{if}\ x_1 \in \rho\ \textbf{then}\ \llbracket s_1 \rrbracket\ \rho(x_1)\ \\ & & \text{and} & ... \\ & & \text{and} &  \textbf{if}\ x_n \in \rho\ \textbf{then}\ \llbracket s_n \rrbracket\ \rho(x_n)
 \end{array}
 {{< /latex >}}
 The first "weird" case now results in the following:
 {{< latex >}}
 \llbracket \texttt{\{} \texttt{x}: \bot \texttt{\}} \rrbracket\ \rho = \textbf{if}\ \texttt{x} \in \rho\ \textbf{then}\ \text{false}
 {{< /latex >}}
 Which is just another way of saying:
 {{< latex >}}
 \llbracket \texttt{\{} \texttt{x}: \bot \texttt{\}} \rrbracket\ \rho = \texttt{x} \notin \rho
 {{< /latex >}}
 In the second case, the interpretation also results in a true statement:
 {{< latex >}}
 \llbracket \texttt{\{} \texttt{x}: + \texttt{\}} \rrbracket\ \rho = \textbf{if}\ \texttt{x} \in \rho\ \textbf{then}\ \texttt{x} > 0
 {{< /latex >}}
 In Agda, I encode the fact that a verified analysis needs a semantic function
 \(\llbracket\cdot\rrbracket\) for its element lattice \(L\) by taking such
 a function as an argument called `⟦_⟧ˡ`:
 {{< codelines "Agda" "agda-spa/Analysis/Forward.agda" 246 253 "hl_lines=5" >}}
 I then define the semantic function for the variable-sign lattice in the following
 way, which eschews the "..." notation in favor of a more Agda-compatible (and
 equivalent) form:
 {{< codelines "Agda" "agda-spa/Analysis/Forward.agda" 255 256 >}}
 The above reads roughly as follows:
 > For every variable `k` and sign [or, more generally, lattice element] `l` in
 > the variable map lattice, if `k` is in the environment `ρ`, then it satisfies
 > the predicate given by the semantic function applied to `l`.
 Let's recap: we have defined a semantic function for our sign lattice, and
 noted that to define a verified analysis, we always need such a semantic function.
 We then showed how to construct a semantic function for a whole variable map
 (of type \(\text{Variable} \to \text{Sign}\), or \(\text{Variable}\to L\)
 in general). We also wrote some Agda code doing all this. As a result, we
 have filled in the missing piece for {{< internalref "correctly-described" >}}property{{< /internalref >}}.
 However, the way that we brought in the semantic function in the Agda code
 above hints that there's more to be discussed. What's `latticeInterpretationˡ`?
 In answering that question, we'll provide evidence for
 {{< internalref "disjunction" >}}property{{< /internalref >}}
 and
 {{< internalref "equivalence" >}}property{{< /internalref >}}.
 ### Properties of the Semantic Function
 As we briefly saw earlier, we loosened the notion of equality to that equivalences,
 which made it possible to ignore things like the ordering of key-value pairs
 in maps. That's great and all, but nothing is stopping us from defining semantic functions that violate our equivalence!
 Supposing \(a \approx f(a)\), as far
 as Agda is concerned, even though \(a\) and \(f(a)\) are "equivalent",
 \(\llbracket a \rrbracket\) and \(\llbracket f(a) \rrbracket\) may be
 totally different. For a semantic function to be correct, it must produce
 the same predicate for equivalent elements of lattice \(L\). That's
 {{< internalref "equivalence" >}}missing piece{{< /internalref >}}.
 Another property of semantic functions that we will need to formalize
 is that \((\sqcup)\) represents disjunction.
 This comes into play when we reason about the correctness of predecessors in
 a Control Flow Graph. Recall that during the last step of processing a given node,
 when we are trying to move on to the next node in the trace, we have knowledge
 that the current node's variable map accurately describes the intermediate
 environment. In other words, \(\llbracket \textit{vs}_i \rrbracket\ \rho_2\) holds, where
 \(\textit{vs}_i\) is the variable map for the current node. We can generalize this
 kowledge a little, and get:
 {{< latex >}}
 \llbracket \textit{vs}_1 \rrbracket\ \rho_2\ \text{or}\ ...\ \text{or}\ \llbracket \textit{vs}_n \rrbracket\ \rho_2
 {{< /latex >}}
 However, the assumption that we _need_ to hold when moving on to a new node
 is in terms of \(\textit{JOIN}\), which combines all the predecessors' maps
 \(\textit{vs}_1, ..., \textit{vs}_n\) using \((\sqcup)\). Thus, we will need to be in a world where
 the following claim is true:
 {{< latex >}}
 \llbracket \textit{vs}_1 \sqcup ... \sqcup \textit{vs}_n \rrbracket\ \rho
 {{< /latex >}}
 To get from one to the other, we will need to rely explicitly on the fact
 that \((\sqcup)\) encodes "or". It's not necessary for the forward analysis,
 but a similar property ought to hold for \((\sqcap)\) and "and". This
 constraint provides {{< internalref "disjunction" >}}missing piece{{< /internalref >}}.
 I defined a new data type that bundles a semantic function with proofs of
 the properties in this section; that's precisely what `latticeInterpretationˡ`
 is:
 {{< codelines "Agda" "agda-spa/Language/Semantics.agda" 66 73 >}}
 In short, to leverage the framework for verified analysis, you would need to
 provide a semantic function that interacts properly with `≈` and `∨`.
 ### Correctness of the Evaluator
 All that's left is {{< internalref "abstract-interpretation" >}}the last missing piece, {{< /internalref >}},
 which requires that `eval` matches the semantics of our language. Recall
 the signature of `eval`:
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 166 166 >}}
 It operates on expressions and variable maps, which themselves associate a
 sign (or, generally, an element of lattice \(L\)), with each variable. The
 "real" evaluation judgement, on the other hand, is in the form
 \(\rho, e \Downarrow v\), and reads "expression \(e\) in environment \(\rho\)
 evaluates to value \(v\)". In Agda:
 {{< codelines "agda" "agda-spa/Language/Semantics.agda" 27 27 >}}
 Let's line up the types of `eval` and the judgement. I'll swap the order of arguments
 for `eval` to make the correspondence easier to see:
 {{< latex >}}
 \begin{array}{ccccccc}
 \text{eval} & : & (\text{Variable} \to \text{Sign}) & \to & \text{Expr} & \to & \text{Sign} \\
 \cdot,\cdot\Downarrow\cdot & : & (\text{Variable} \to \text{Value}) & \to & \text{Expr} & \to & \text{Value} & \to & \text{Set} \\
 & & \underbrace{\phantom{(\text{Variable} \to \text{Value})}}_{\text{environment-like inputs}} & & & & \underbrace{\phantom{Value}}_{\text{value-like outputs}}
 \end{array}
 {{< /latex >}}
 Squinting a little, it's almost like the signature of `eval` is the signature
 for the evaluation judgement, but it forgets a few details (the exact values
 of the variables) in favor of abstractions (their signs). To show that `eval`
 behaves correctly, we'll want to prove that this forgetful correspondence holds.
 Concretely, for any expression \(e\), take some environment \(\rho\), and "forget"
 the exact values, getting a sign map \(\textit{vs}\). Now, evaluate the expression
 to some value \(v\) using the semantics, and also, compute the expression's
 expected sign \(s\) using `eval`. The sign should be the same as forgetting
 \(v\)'s exact value. Mathematically,
 {{< latex >}}
 \forall e, \rho, v, \textit{vs}.\ \textbf{if}\ \llbracket\textit{vs}\rrbracket \rho\ \text{and}\ \rho, e \Downarrow v\ \textbf{then}\ \llbracket \text{eval}\ \textit{vs}\ e\rrbracket v
 {{< /latex >}}
 In Agda:
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 286 287 >}}
 For a concrete analysis, we need to prove the above claim. In the case of
 sign analysis, this boils down to a rather cumbersome proof by cases. I will collapse
 the proofs to save some space and avoid overwhelming the reader.
 {{< codelines "agda" "agda-spa/Analysis/Sign.agda" 237 258 "" "**(Click here to expand the proof of correctness for plus)**" >}}
 {{< codelines "agda" "agda-spa/Analysis/Sign.agda" 261 282 "" "**(Click here to expand the proof of correctness for minus)**" >}}
 {{< codelines "agda" "agda-spa/Analysis/Sign.agda" 284 294 "" >}}
 This completes {{< internalref "abstract-interpretation" >}}our last missing piece,{{< /internalref >}}.
 All that's left is to put everything together.
 ### Proving The Analysis Correct
 #### Lifting Expression Evaluation Correctness to Statements
 The individual analyses (like the sign analysis) provide only an evaluation
 function for _expressions_, and thus only have to prove correctness of
 that function. However, our language is made up of statements, with judgements
 in the form \(\rho, s \Rightarrow \rho'\). Now that we've shown (or assumed)
 that `eval` behaves correctly when evaluating expressions, we should show
 that this correctness extends to evaluating statements, which in the
 forward analysis implementation is handled by the
 [`updateVariablesFromStmt` function]({{< relref "08_spa_agda_forward#define-updateVariablesFromStmt" >}}).
 The property we need to show looks very similar to the property for `eval`:
 {{< latex >}}
 \forall b, \rho, \rho', \textit{vs}.\ \textbf{if}\ \llbracket\textit{vs}\rrbracket \rho\ \text{and}\ \rho, b \Rightarrow \rho'\ \textbf{then}\ \llbracket \text{updateVariablesFromStmt}\ \textit{vs}\ b\rrbracket \rho'
 {{< /latex >}}
 In Agda:
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 291 291 >}}
 The proof is straightforward, and relies on the semantics of the [map update]({{< relref "08_spa_agda_forward#generalized-update" >}}).
 Specifically, in the case of an assignment statement \(x \leftarrow e\), all we
 do is store the new sign computed from \(e\) into the map at \(x\). To
 prove the correctness of the entire final environment \(\rho'\), there are
 two cases to consider:
 * A variable in question is the newly-updated \(x\). In this case, since
  `eval` produces correct signs, the variable clearly has the correct sign.
  This is the first highlighted chunk in the below code.
 * A variable in question is different from \(x\). In this case, its value
  in the environment \(\rho'\) should be the same as it was prior, and
  its sign in the updated variable map is the same as it was in the original.
  Since the original map correctly described the original environment, we know
  the sign is correct. This is the second highlighted chunk in the below
  code.
 The corresponding Agda proof is as follows:
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 291 305 "hl_lines=5-7 10-15" >}}
 From this, it follows with relative ease that each basic block in the lattice,
 when evaluated, produces an environment that matches the prediction of our
 forward analysis.
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 318 318 >}}
 #### Walking the Trace
 Finally, we get to the meat of the proof, which follows the [outline](#high-level-algorithm). First,
 let's take a look at `stepTrace`, which implements the second bullet in
 our iterative procedure. I'll show the code, then we can discuss it
 in detail.
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 324 342 >}}
 The first `let`-bound variable, `⟦joinAll-result⟧ρ₁` is kind of an intermediate
 result, which I was forced to introduced because `rewrite` caused Agda to
 allocate ~100GB of memory. It simply makes use of the fact that `joinAll`, the
 function that performs predecessor joining for each node in the CFG, sets
 every key of the map accordingly.
 The second `let`-bound variable, `⟦analyze-result⟧`, steps through a given
 node's basic block and leverages our proof of statement-correctness to validate
 that the final environment `ρ₂` matches the predication of the analyzer.
 The last two `let`-bound variables apply the equation we wrote above:
 {{< latex >}}
 r = \text{update}(\text{join}(r))
 {{< /latex >}}
 Recall that `analyze` is the combination of `update` and `join`:
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 226 227 >}}
 Finally, the `in` portion of the code uses `⟦⟧ᵛ-respects-≈ᵛ`, a proof
 of {{< internalref "equivalence" >}}property{{< /internalref >}}, to produce
 the final claim in terms of the `result` map.
 Knowing how to step, we can finally walk the entire trace, implementing
 the iterative process:
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 344 357 >}}
 The first step --- assuming that one of the predecessors of the
 current node satisfies the initial environment `ρ₁` --- is captured by
 the presence of the argument `⟦joinForKey-s₁⟧ρ₁`. We expect the calling code
 to provide a proof of that.
 The second step, in both cases, is implemented using `stepTrace`,
 as we saw above. That results in a proof that at the end of the current basic
 block, the final environment `ρ₂` is accurately described.
 From there, we move on to the third iterative step, if necessary. The
 sub-expression `edge⇒incoming s₁→s₂` validates that, since we have an edge
 from the current node to the next, we are listed as a predecessor. This,
 in turn, means that we are included in the list of states-to-join for the
 \(\textit{JOIN}\) function. That fact is stored in `s₁∈incomingStates`.
 Finally, relying on
 {{< internalref "disjunction" >}}property{{< /internalref >}},
 we construct an assumption fit for a recursive invocation of `walkTrace`,
 and move on to the next CFG node. The `foldr` here is motivated by the fact
 that "summation" using \((\sqcup)\) is a fold.
 When the function terminates, what we have is a proof that the final program
 state is accurately described by the results of our program analysis. All
 that's left is to kick off the walk. To do that, observe that the initial state
 has no predecessors (how could it, if it's at the beginning of the program?).
 That, in turn, means that this state maps every variable to the bottom element.
 Such a variable configuration only permits the empty environment \(\rho = \varnothing\).
 If the program evaluation starts in an empty environment, we have the assumption
 needed to kick off the iteration.
 {{< codelines "agda" "agda-spa/Analysis/Forward.agda" 359 366 "hl_lines=7" >}}
 Take a look at the highlighted line in the above code block in particular.
 It states precisely what we were hoping to see: that, when evaluating
 a program, the final state when it terminates is accurately described by
 the `result` of our static program analysis at the `finalState` in the CFG.
 We have done it!
 ### Future Work
 It took a lot of machinery to get where we are, but there's still lots of
 things to do.
 1. __Correctness beyond the final state__: the statement we've arrived at
   only shows that the final state of the program matches the results of
   the analysis. In fact, the property hold for all intermediate states, too.
   The only snag is that it's more difficult to _state_ such a claim.
   To do something like that, we probably need a notion of "incomplete evaluations"
   of our language, which run our program but stop at some point before the end.
   A full execution would be a special case of such an "incomplete evaluation"
   that stops in the final state. Then, we could restate `analyze-correct`
   in terms of partial evaluations, which would strengthen it.
 2. __A more robust language and evaluation process__: we noted above that
   our join-based analysis is a little bit weird, particularly in the
   cases of uninitialized variables. There are ways to adjust our language
   (e.g., introducing variable declaration points) and analysis functions
   (e.g., only allowing assignment for declared variables) to reduce
   the weirdness somewhat. They just lead to a more complicated language.
 3. __A more general correctness condition__: converting lattice elements into
   predicates on values gets us far. However, some types of analyses make claims
   about more than the _current_ values of variables. For instance, _live variable
   analysis_ checks if a variable's current value is going to be used in the
   future. Such an analysis can help guide register (re)allocation. To
   talk about future uses of a variable, the predicate will need to be formulated
   in terms of the entire evaluation proof tree. This opens a whole can
   of worms that I haven't begun to examine.
 Now that I'm done writing up my code so far, I will start exploring these
 various avenues of work. In the meantime, though, thanks for reading!
--- a/content/blog/12_compiler_let_in_lambda/thumbnail.png
+++ b/content/blog/12_compiler_let_in_lambda/thumbnail.png
--- a/content/blog/bergamot/thumbnail.png
+++ b/content/blog/bergamot/thumbnail.png
--- a/content/blog/chapel_runtime_types.md
+++ b/content/blog/chapel_runtime_types.md
@@ -0,0 +1,591 @@
 ---
 title: "Chapel's Runtime Types as an Interesting Alternative to Dependent Types"
 date: 2025-03-02T22:52:01-08:00
 tags: ["Chapel", "C++", "Idris", "Programming Languages"]
 description: "In this post, I discuss Chapel's runtime types as a limited alternative to dependent types."
 ---
 One day, when I was in graduate school, the Programming Languages research
 group was in a pub for a little gathering. Amidst beers, fries, and overpriced
 sandwiches, the professor and I were talking about [dependent types](https://en.wikipedia.org/wiki/Dependent_type). Speaking
 loosely and imprecisely, these are types that are somehow constructed from
 _values_ in a language, like numbers.
 For example, in C++, [`std::array`](https://en.cppreference.com/w/cpp/container/array)
 is a dependent type. An instantiation of the _type_ `array`, like `array<string, 3>`
 is constructed from the type of its elements (here, `string`) and a value
 representing the number of elements (here, `3`). This is in contrast with types
 like `std::vector`, which only depends on a type (e.g., `vector<string>` would
 be a dynamically-sized collection of strings).
 I was extolling the virtues of general dependent types, like you might find
 in [Idris](https://www.idris-lang.org/) or [Agda](https://agda.readthedocs.io/en/latest/getting-started/what-is-agda.html):
 more precise function signatures! The
 {{< sidenote "right" "curry-howard-note" "Curry-Howard isomorphism!" >}}
 The Curry-Howard isomorphism is a common theme on this blog. I've
 <a href="{{< relref "typesafe_interpreter_revisited#curry-howard-correspondence" >}}">
 written about it myself</a>, but you can also take a look at the
 <a href="https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence">
 Wikipedia page</a>.
 {{< /sidenote >}} The professor was skeptical. He had been excited about
 dependent types in the past, but nowadays he felt over them. They were cool, he
 said, but there are few practical uses. In fact, he posed a challenge:
 > Give me one good reason to use dependent types in practice that doesn't
 > involve keeping track of bounds for lists and matrices!
 {#bounds-quote}
 This challenge alludes to fixed-length lists -- [vectors](https://agda.github.io/agda-stdlib/master/Data.Vec.html)
 -- which are one of the first dependently-typed data structures one learns about.
 Matrices are effectively vectors-of-vectors. In fact, even in giving my introductory
 example above, I demonstrated the C++ equivalent of a fixed-length list, retroactively
 supporting the professor's point.
 It's not particularly important to write down how I addressed the challenge;
 suffice it to say that the notion resonated with some of the other
 students present in the pub. In the midst of practical development, how much
 of dependent types' power can you leverage, and how much power do you pay
 for but never use?
 A second round of beers arrived. The argument was left largely unresolved,
 and conversation flowed to other topics. Eventually, I graduated, and started
 working on the [Chapel language](https://chapel-lang.org/) team (I also
 [write on the team's blog](https://chapel-lang.org/blog/authors/daniel-fedorin/)).
 When I started looking at Chapel programs, I could not believe my eyes...
 ### A Taste of Chapel's Array Types
 Here's a simple Chapel program that creates an array of 10 integers.
 ```Chapel
 var A: [0..9] int;
 ```
 Do you see the similarity to the `std::array` example above? Of course, the
 syntax is quite different, but in _essence_ I think the resemblance is
 uncanny. Let's mangle the type a bit --- producing invalid Chapel programs ---
 just for the sake of demonstration.
 ```Chapel
 var B: array(0..9, int); // first, strip the syntax sugar
 var C: array(int, 0..9); // swap the order of the arguments to match C++
 ```
 Only one difference remains: in C++, arrays are always indexed from zero. Thus,
 writing `array<int, 10>` would implicitly create an array whose indices start
 with `0` and end in `9`. In Chapel, array indices can start at values other
 than zero (it happens to be useful for elegantly writing numerical programs),
 so the type explicitly specifies a lower and a higher bound. Other than that,
 though, the two types look very similar.
 In general, Chapel arrays have a _domain_, typically stored in variables like `D`.
 The domain of `A` above is `{0..9}`. This domain is part of the array's type.
 Before I move on, I'd like to pause and state a premise that is crucial
 for the rest of this post: __I think knowing the size of a data structure,
 like `std::array` or Chapel's `[0..9] int`, is valuable__. If this premise
 were not true, there'd be no reason to prefer `std::array` to `std::vector`, or
 care that Chapel has indexed arrays. However, having this information
 can help in numerous ways, such as:
 * __Enforcing compatible array shapes.__ For instance, the following Chapel
  code would require two arrays passed to function `foo` to have the same size.
  ```Chapel
  proc doSomething(people: [?D] person, data: [D] personInfo) {}
  ```
  Similarly, we can enforce the fact that an input to a function has the same shape
  as the output:
  ```Chapel
  proc transform(input: [?D] int): [D] string;
  ```
 * __Consistency in generics__. Suppose you have a generic function that declares
  a new variable of a given type, and just returns it:
  ```Chapel
  proc defaultValue(type argType) {
    var x: argType;
    return x;
  }
  ```
  Code like this exists in "real" Chapel software, by the way --- the example
  is not contrived. By including the bounds etc. into the array type, we can
  ensure that `x` is appropriately allocated. Then, `defaultValue([1,2,3].type)`
  would return an array of three default-initialized integers.
 * __Eliding boundary checking__. Boundary checking is useful for safety,
  since it ensures that programs don't read or write past the end of allocated
  memory. However, bounds checking is also slow. Consider the following function that
  sums two arrays:
  ```Chapel
  proc sumElementwise(A: [?D] int, B: [D] int) {
    var C: [D] int;
    for idx in D do
      C[idx] = A[idx] + B[idx];
  }
  ```
  Since arrays `A`, `B`, and `C` have the same domain `D`, we don't need
  to do bound checking when accessing any of their elements. I don't believe
  this is currently an optimisation in Chapel, but it's certainly on the
  table.
 * __Documentation__. Including the size of the array as part of type
  signature clarifies the intent of the code being written. For instance,
  in the following function:
  ```Chapel
  proc sendEmails(numEmails: int, destinationAddrs: [1..numEmails] address) { /* ... */ }
  ```
  It's clear from the type of the `destinationAddrs`s that there ought to
  be exactly as many `destinationAddrs` as the number of emails that should
  be sent.
 Okay, recap: C++ has `std::array`, which is a dependently-typed container
 that represents an array with a fixed number of elements. Chapel has something
 similar. I think these types are valuable.
 At this point, it sort of looks like I'm impressed with Chapel for copying a C++
 feature from 2011. Not so! As I played with Chapel programs more and more,
 arrays miraculously supported patterns that I knew I couldn't write in C++.
 The underlying foundation of Chapel's array types is quite unlike any other.
 Before we get to that, though, let's take a look at how dependent types
 are normally used (by us mere mortal software engineers).
 ### Difficulties with Dependent Types
 Let's start by looking at a simple operation on fixed-length lists: reversing them.
 One might write a reverse function for "regular" lists, ignoring details
 like ownership, copying, that looks like this:
 ```C++
 std::vector<int> reverse(std::vector<int>);
 ```
 This function is not general: it won't help us reverse lists of
 strings, for instance. The "easy fix" is to replace `int` with some kind
 of placeholder that can be replaced with any type.
 ```C++
 std::vector<T> reverse(std::vector<T>);
 ```
 You can try compiling this code, but you will immediately run into an error.
 What the heck is `T`? Normally,
 when we name a variable, function, or type (e.g., by writing `vector`, `reverse`),
 we are referring to its declaration somewhere else. At this time, `T` is not
 declared anywhere. It just "appears" in our function's type. To fix this,
 we add a declaration for `T` by turning `reverse` into a template:
 ```C++
 template <typename T>
 std::vector<T> reverse(std::vector<T>);
 ```
 The new `reverse` above takes two arguments: a type and a list of values of
 that type. So, to _really_ call this `reverse`, we need to feed the type
 of our list's elements into it. This is normally done automatically
 (in C++ and otherwise) but under the hood, invocations might look like this:
 ```C++
 reverse<int>({1,2,3});              // produces 3, 2, 1
 reverse<string>({"world", "hello"}) // produces "hello", "world"
 ```
 This is basically what we have to do to write `reverse` on `std::array`, which,
 includes an additional parameter that encodes its length. We might start with
 the following (using `n` as a placeholder for length, and observing that
 reversing an array doesn't change its length):
 ```C++
 std::array<T, n> reverse(std::array<T, n>);
 ```
 Once again, to make this compile, we need to add template parameters for `T` and `n`.
 ```C++
 template <typename T, size_t n>
 std::array<T, n> reverse(std::array<T, n>);
 ```
 Now, you might be asking...
 {{< dialog >}}
 {{< message "question" "reader" >}}
 This section is titled "Difficulties with Dependent Types". What's the difficulty?
 {{< /message >}}
 {{< /dialog >}}
 Well, here's the kicker. C++ templates are a __compile-time mechanism__. As
 a result, arguments to `template` (like `T` and `n`) must be known when the
 program is being compiled. This, in turn, means
 {{< sidenote "right" "deptype-note" "the following program doesn't work:" >}}
 The observant reader might have noticed that one of the Chapel programs we
 saw above, <code>sendEmails</code>, does something similar. The
 <code>numEmails</code> argument is used in the type of the
 <code>destinationAddrs</code> parameter. That program is valid Chapel.
 {{< /sidenote >}}
 ```C++
 void buildArray(size_t len) {
  std::array<int, len> myArray;
  // do something with myArray
 }
 ```
 You can't use these known-length types like `std::array` with any length
 that is not known at compile-time. But that's a lot of things! If you're reading
 from an input file, chances are, you don't know how big that file is. If you're
 writing a web server, you likely don't know the length the HTTP requests.
 With every setting a user can tweak when running your code, you sacrifice the
 ability to use templated types.
 Also, how do you _return_ a `std::array`? If the size of the returned array is
 known in advance, you just list that size:
 ```C++
 std::array<int, 10> createArray();
 ```
 If the size is not known at compile-time, you might want to do something like
 the following --- using an argument `n` in the type of the returned array ---
 but it would not compile:
 ```C++
 auto computeNNumbers(size_t n) -> std::array<int, n>; // not valid C++
 ```
 Moreover, you actually can't use `createArray` to figure out the required
 array size, and _then_ return an array that big, even if in the end you
 only used compile-time-only computations in the body of `createArray`.
 What you would need is to provide a "bundle" of a value and a type that is somehow
 built from that value.
 ```C++
 // magic_pair is invented syntax, will not even remotely work
 auto createArray() -> magic_pair<size_t size, std::array<int, size>>;
 ```
 This pair contains a `size` (suppose it's known at compilation time for
 the purposes of appeasing C++) as well as an array that uses that `size`
 as its template argument. This is not real C++ -- not even close -- but
 such pairs are a well-known concept. They are known as
 [dependent pairs](https://unimath.github.io/agda-unimath/foundation.dependent-pair-types.html),
 or, if you're trying to impress people, \(\Sigma\)-types. In Idris, you
 could write `createArray` like this:
 ```Idris
 createArray : () -> (n : Nat ** Vec n Int)
 ```
 There are languages out there -- that are not C++, alas -- that support
 dependent pairs, and as a result make it more convenient to use types that
 depend on values. Not only that, but a lot of these languages do not force
 dependent types to be determined at compile-time. You could write that
 coveted `readArrayFromFile` function:
 ```Idris
 readArrayFromFile : String -> IO (n : Nat ** Vec n String)
 ```
 Don't mind `IO`; in pure languages like Idris, this type is a necessity when
 interacting when reading data in and sending it out. The key is that
 `readArrayFromFile` produces, at runtime, a pair of `n`, which is the size
 of the resulting array, and a `Vec` of that many `String`s (e.g., one string
 per line of the file).
 Dependent pairs are cool and very general. However, the end result of
 types with bounds which are not determined at compile-time is that you're
 _required_ to use dependent pairs. Thus, you must always carry the array's length
 together with the array itself.
 The bottom line is this:
 * In true dependently typed languages, a type that depends on a value (like `Vec`
  in Idris) lists that value in its type. When this value is listed by
  referring to an identifier --- like `n` in `Vec n String` above --- this
  identifier has to be defined somewhere, too. This necessitates dependent pairs,
  in which the first element is used syntactically as the "definition point"
  of a type-level value. For example, in the following piece of code:
  ```Idris
  (n : Nat ** Vec n String)
  ```
  The `n : Nat` part of the pair serves both to say that the first element
  is a natural number, and to introduce a variable `n` that refers to
  this number so that the second type (`Vec n String`) can refer to it.
  A lot of the time, you end up carrying this extra value (bound to `n` above)
  with your type.
 * In more mainstream languages, things are even more restricted: dependently
  typed values are a compile-time property, and thus, cannot be used with
  runtime values like data read from a file, arguments passed in to a function,
  etc..
 ### Hiding Runtime Values from the Type
 Let's try to think of ways to make things more convenient. First of all, as
 we saw, in Idris, it's possible to use runtime values in types. Not only that,
 but Idris is a compiled language, so presumably we can compile dependently typed programs
 with runtime-enabled dependent types. The trick is to forget some information:
 turn a vector `Vec n String` into two values (the size of the vector and the
 vector itself), and forget -- for the purposes of generating code -- that they're
 related. Whenever you pass in a `Vec n String`, you can compile that similarly
 to how you'd compile passing in a `Nat` and `List String`. Since the program has
 already been type checked, you can be assured that you don't encounter cases
 when the size and the actual vector are mismatched, or anything else of that
 nature.
 Additionally, you don't always need the length of the vector at all. In a
 good chunk of Idris code, the size arguments are only used to ensure type
 correctness and rule out impossible cases; they are never accessed at runtime.
 As a result, you can _erase_ the size of the vector altogether. In fact,
 [Idris 2](https://github.com/idris-lang/Idris2/) leans on [Quantitative Type Theory](https://bentnib.org/quantitative-type-theory.html)
 to make erasure easier.
 At this point, one way or another, we've "entangled" the vector with a value
 representing its size:
 * When a vector of some (unknown, but fixed) length needs to be produced from
  a function, we use dependent pairs.
 * Even in other cases, when compiling, we end up treating a vector as a
  length value and the vector itself.
 Generally speaking, a good language design practice is to hide extraneous
 complexity, and to remove as much boilerplate as necessary. If the size
 value of a vector is always joined at the hip with the vector, can we
 avoid having to explicitly write it?
 This is pretty much exactly what Chapel does. It _allows_ explicitly writing
 the domain of an array as part of its type, but doesn't _require_ it. When
 you do write it (re-using my original snippet above):
 ```Chapel
 var A: [0..9] int;
 ```
 What you are really doing is creating a value (the [range](https://chapel-lang.org/docs/primers/ranges.html) `0..9`),
 and entangling it with the type of `A`. This is very similar to what a language
 like Idris would do under the hood to compile a `Vec`, though it's not quite
 the same.
 At the same time, you can write code that omits the bounds altogether:
 ```Chapel
 proc processArray(A: [] int): int;
 proc createArray(): [] int;
 ```
 In all of these examples, there is an implicit runtime value (the bounds)
 that is associated with the array's type. However, we are never forced to
 explicitly thread through or include a size. Where reasoning about them is not
 necessary, Chapel's domains are hidden away. Chapel refers to the implicitly
 present value associated with an array type as its _runtime type_.
 I hinted earlier that things are not quite the same in this representation
 as they are in my simplified model of Idris. In Idris, as I mentioned earlier,
 the values corresponding to vectors' indices can be erased if they are not used.
 In Chapel, this is not the case --- a domain always exists at runtime. At the
 surface level, this means that you may pay for more than what you use. However,
 domains enable a number of interesting patterns of array code. We'll get
 to that in a moment; first, I want to address a question that may be on
 your mind:
 {{< dialog >}}
 {{< message "question" "reader" >}}
 At this point, this looks just like keeping a <code>.length</code> field as
 part of the array value. Most languages do this. What's the difference
 between this and Chapel's approach?
 {{< /message >}}
 {{< /dialog >}}
 This is a fair question. The key difference is that the length exists even if an array
 does not. The following is valid Chapel code (re-using the `defaultValue`
 snippet above):
 ```Chapel
 proc defaultValue(type argType) {
  var x: argType;
  return x;
 }
 proc doSomething() {
  type MyArray = [1..10] int;
  var A = defaultValue(MyArray);
 }
 ```
 Here, we created an array `A` with the right size (10 integer elements)
 without having another existing array as a reference. This might seem like
 a contrived example (I could've just as well written `var A: [1..10] int`),
 but the distinction is incredibly helpful for generic programming. Here's
 a piece of code from the Chapel standard library, which implements
 a part of Chapel's [reduction](https://chapel-lang.org/docs/primers/reductions.html) support:
 {{< githubsnippet "chapel-lang/chapel" "e8ff8ee9a67950408cc6d4c3220ac647817ddae3" "modules/internal/ChapelReduce.chpl" "Chapel" 146 >}}
    inline proc identity {
      var x: chpl__sumType(eltType); return x;
    }
 {{< /githubsnippet >}}
 Identity elements are important when performing operations like sums and products,
 for many reasons. For one, they tell you what the sum (e.g.) should be when there
 are no elements at all. For another, they can be used as an initial value for
 an accumulator. In Chapel, when you are performing a reduction, there is a
 good chance you will need several accumulators --- one for each thread performing
 a part of the reduction.
 That `identity` function looks almost like `defaultValue`! Since it builds the
 identity element from the type, and since the type includes the array's dimensions,
 summing an array-of-arrays, even if it's empty, will produce the correct output.
 ```Chapel
 type Coordinate = [1..3] real;
 var Empty: [0..<0] Coordinate;
 writeln(+ reduce Empty); // sum up an empty list of coordinates
 ```
 As I mentioned before, having the domain be part of the type can also enable
 indexing optimizations --- without any need for [interprocedural analysis](https://en.wikipedia.org/wiki/Interprocedural_optimization) ---
 in functions like `sumElementwise`:
 ```Chapel
 proc sumElementwise(A: [?D] int, B: [D] int) {
  var C: [D] int;
  for idx in D do
    C[idx] = A[idx] + B[idx];
 }
 ```
 The C++ equivalent of this function -- using `vectors` to enable arbitrary-size
 lists of numbers read from user input, and `.at` to enable bounds checks ---
 does not include enough information for this optimization to be possible.
 ```C++
 void sumElementwise(std::vector<int> A, std::vector<int> B) {
  std::vector<int> C(A.size());
  for (size_t i = 0; i < A.size(); i++) {
    C.at(i) = A.at(i) + B.at(i);
  }
 }
 ```
 All in all, this makes for a very interesting mix of features:
 * __Chapel arrays have their bounds as part of types__, like `std::array` in C++
  and `Vec` in Idris. This enables all the benefits I've described above.
 * __The bounds don't have to be known at compile-time__, like all dependent
  types in Idris. This means you can read arrays from files (e.g.) and still
  reason about their bounds as part of the type system.
 * __Domain information can be hidden when it's not used__, and does not require
  explicit additional work like template parameters or dependent pairs.
 Most curiously, runtime types only extend to arrays and domains. In that sense,
 they are not a general purpose replacement for dependent types. Rather,
 they make arrays and domains special, and single out the exact case my
 professor was [talking about in the introduction](#bounds-quote). Although
 at times I've [twisted Chapel's type system in unconventional ways](https://chapel-lang.org/blog/posts/linear-multistep/)
 to simulate dependent types, rarely have I felt a need for them while
 programming in Chapel. In that sense --- and in the "practical software engineering"
 domain --- I may have been proven wrong.
 ### Pitfalls of Runtime Types
 Should all languages do things the way Chapel does? I don't think so. Like
 most features, runtime types like that in Chapel are a language design
 tradeoff. Though I've covered their motivation and semantics, perhaps
 I should mention the downsides.
 The greatest downside is that, generally speaking, _types are not always a
 compile-time property_. We saw this earlier with `MyArray`:
 ```Chapel
 type MyArray = [1..10] int;
 ```
 Here, the domain of `MyArray` (one-dimensional with bounds `1..10`) is a runtime
 value. It has an
 {{< sidenote "right" "dce-note" "execution-time cost." >}}
 The execution-time cost is, of course, modulo <a href="https://en.wikipedia.org/wiki/Dead-code_elimination">dead code elimination</a> etc.. If
 my snippet made up the entire program being compiled, the end result would
 likely do nothing, since <code>MyArray</code> isn't used anywhere.
 {{< /sidenote >}}
 Moreover, types that serve as arguments to functions (like `argType` for
 `defaultValue`), or as their return values (like the result of `chpl__sumType`)
 also have an execution-time backing. This is quite different from most
 compiled languages. For instance, in C++, templates are "stamped out" when
 the program is compiled. A function with a `typename T` template parameter
 called with type `int`, in terms of generated code, is always the same as
 a function where you search-and-replaced `T` with `int`. This is called
 [monomorphization](https://en.wikipedia.org/wiki/Monomorphization), by the
 way. In Chapel, however, if the function is instantiated with an array type,
 it will have an additional parameter, which represents the runtime component
 of the array's type.
 The fact that types are runtime entities means that compile-time type checking
 is insufficient. Take, for instance, the above `sendEmails` function:
 ```Chapel
 proc sendEmails(numEmails: int, destinationAddrs: [1..numEmails] address) { /* ... */ }
 ```
 Since `numEmails` is a runtime value (it's a regular argument!), we can't ensure
 at compile-time that a value of some array matches the `[1..numEmails] address`
 type. As a result, Chapel defers bounds checking to when the `sendEmails`
 function is invoked.
 This leads to some interesting performance considerations. Take two Chapel records
 (similar to `struct`s in C++) that simply wrap a value. In one of them,
 we provide an explicit type for the field, and in the other, we leave the field
 type generic.
 ```Chapel
 record R1 { var field: [1..10] int; }
 record R2 { var field; }
 var A = [1,2,3,4,5,6,7,8,9,10];
 var r1 = new R1(A);
 var r2 = new R2(A);
 ```
 In a conversation with a coworker, I learned that these are not the same.
 That's because the record `R1` explicitly specifies a type
 for `field`. Since the type has a runtime component, the constructor
 of `R1` will actually perform a runtime check to ensure that the argument
 has 10 elements. `R2` will not do this, since there isn't any other type
 to check against.
 Of course, the mere existence of an additional runtime component is a performance
 consideration. To ensure that Chapel programs perform as well as possible,
 the Chapel standard library attempts to avoid using runtime components
 wherever possible. This leads to a distinction between a "static type"
 (known at compile-time) and a "dynamic type" (requiring a runtime value).
 The `chpl__sumType` function we saw mentioned above uses static components of
 types, because we don't want each call to `+ reduce` to attempt to run a number
 of extraneous runtime queries.
 ### Conclusion
 Though runtime types are not a silver bullet, I find them to be an elegant
 middle-ground solution to the problem of tracking array bounds. They enable
 optimizations, generic programming, and more, without the complexity of
 a fully dependently-typed language. They are also quite unlike anything I've
 seen in any other language.
 What's more, this post only scratches the surface of what's possible using
 arrays and domains. Besides encoding array bounds, domains include information
 about how an array is distributed across several nodes (see the
 [distributions primer](https://chapel-lang.org/docs/primers/distributions.html)),
 and how it's stored in memory (see the [sparse computations](https://chapel-lang.org/blog/posts/announcing-chapel-2.3/#sparse-computations)
 section of the recent 2.3 release announcement). In general, they are a very
 flavorful component to Chapel's "special sauce" as a language for parallel
 computing.
 You can read more about arrays and domains in the [corresponding primer](https://chapel-lang.org/docs/primers/arrays.html).
--- a/content/blog/codelines/thumbnail.png
+++ b/content/blog/codelines/thumbnail.png
--- a/content/blog/coq_dawn_eval/thumbnail.png
+++ b/content/blog/coq_dawn_eval/thumbnail.png
--- a/content/blog/dyno_alloy/thumbnail.png
+++ b/content/blog/dyno_alloy/thumbnail.png
--- a/content/blog/haskell_lazy_evaluation/thumbnail.png
+++ b/content/blog/haskell_lazy_evaluation/thumbnail.png
--- a/content/blog/i_love_programming_languages/cardeli-products.png
+++ b/content/blog/i_love_programming_languages/cardeli-products.png
--- a/content/blog/i_love_programming_languages/index.md
+++ b/content/blog/i_love_programming_languages/index.md
@@ -0,0 +1,415 @@
 ---
 title: "Reasons to Love the Field of Programming Languages"
 date: 2025-12-31
 tags: ["Programming Languages", "Compilers", "Type Systems"]
 ---
 I work at HPE on the
 [Chapel Programming Language](https://chapel-lang.org). Recently, another HPE
 person asked me:
 > So, you work on the programming language. What's next for you?
 This caught me off-guard because I hadn't even conceived of moving on.
 I don't want to move on, because __I love the field of programming languages__.
 In addition, I have come to think there is something in PL for everyone, from
 theorists to developers to laypeople.
 So, in that spirit, I am writing this list as a non-exhaustive survey that holds
 the dual purpose of explaining my personal infatuation with PL, and providing
 others with ways to engage with PL that align with their existing interests.
 I try to provide rationale for each claim, but you can just read the reasons
 themselves and skip the rest.
 My general thesis goes something like this: programming languages are a unique
 mix of the __inherently human and social__ and the __deeply mathematical__,
 a mix that often remains deeply grounded in the practical, __low-level realities of
 our hardware__.
 Personally, I find all of these properties equally important, but we have to
 start somewhere. Let's begin with the human aspect of programming languages.
 ### Human Aspects of PL
 > Programs must be written for people to read, and only incidentally for machines
 > to execute.
 >
 > --- Abelson & Sussman, _Structure and Interpretation of Computer Programs_.
 As we learn more about the other creatures that inhabit our world, we discover
 that they are similar to us in ways that we didn't expect. However, our
 language is unique to us. It gives us the ability to go far beyond
 the simple sharing of information: we communicate abstract concepts,
 social dynamics, stories. In my view, storytelling is our birthright more
 so than anything else.
 I think this has always been reflected in the broader discipline of programming.
 _Code should always tell a story_, I've heard throughout my education and career.
 _It should explain itself_. In paradigms such as
 [literate programming](https://en.wikipedia.org/wiki/Literate_programming),
 we explicitly mix prose and code. Notebook technologies
 like [Jupyter](https://jupyter.org/) intersperse computation with explanations
 thereof.
 * __Reason 1__: programming languages provide the foundation of expressing
  human thought and stories through code.
 From flowery prose to clinical report, human expression takes a wide variety
 of forms. The need to vary our descriptions is also well-served by the diversity
 of PL paradigms. From stateful transformations in languages like Python and C++,
 through pure and immutable functions in Haskell and Lean, to fully declarative
 statements-of-fact in Nix, various languages have evolved to
 support the many ways in which we wish to describe our world and our needs.
 * __Reason 2__: diverse programming languages enable different perspectives
  and ways of storytelling, allowing us choice in how to express our thoughts
  and solve our problems.
 Those human thoughts of ours are not fundamentally grounded in logic,
 mathematics, or anything else. They are a product of millennia of evolution
 through natural selection, of adaptation to ever-changing conditions.
 Our cognition is limited, rife with blind spots, and partial to the subject
 matter at hand. We lean on objects, actors, contracts, and more as helpful,
 mammal-compatible analogies. I find this to be beautiful; here is something
 we can really call ours.
 * __Reason 3__: programming languages imbue the universe's fundamental rules of
  computation with humanity's identity and idiosyncrasies. They carve out
  a home for us within impersonal reality.
 Storytelling (and, more generally, writing) is not just about communicating
 with others. Writing helps clarify one's own thoughts, and to think deeper.
 In his 1979 Turing Award lecture,
 [Notation as a Tool of Thought](https://www.eecg.utoronto.ca/~jzhu/csc326/readings/iverson.pdf),
 Kenneth Iverson, the creator of [APL](https://tryapl.org/), highlighted ways
 in which programming languages, with their notation, can help express patterns
 and facilitate thinking.
 Throughout computing history, programming languages built abstractions that ---
 together with advances in hardware --- made it possible to create ever more
 complex software. Dijkstra's
 [structured programming](https://en.wikipedia.org/wiki/Structured_programming)
 crystallized the familiar patterns of `if`/`else` and `while` out of
 a sea of control flow. Structures and objects partitioned data and state
 into bundles that could be reasoned about, or put out of mind when irrelevant.
 Recently, I dare say that notions of ownership and lifetimes popularized
 by Rust have clarified how we think about memory.
 * __Reason 4__: programming languages combat complexity, and give us tools to
  think and reason about unwieldy and difficult problems.
 The fight against complexity occurs on more battlegrounds than PL design alone.
 Besides its syntax and semantics, a programming language is comprised of its
 surrounding tooling: its interpreter or compiler, perhaps its package manager
 or even its editor. Language designers and developers take great care to
 [improve the quality of error messages](https://elm-lang.org/news/compiler-errors-for-humans),
 to provide [convenient editor tooling](https://chapel-lang.org/blog/posts/chapel-lsp/),
 and build powerful package managers
 like [Yarn](https://yarnpkg.com/). Thus, in each language project, there is
 room for folks who, even if they are not particularly interested in grammars or
 semantics, care about the user experience.
 * __Reason 5__: programming languages provide numerous opportunities for
  thoughtful forays into the realms of User Experience and Human-Computer
  Interaction.
 I hope you agree, by this point, that programming languages are fundamentally
 tethered to the human. Like any human endeavor, then, they don't exist in
 isolation. To speak a language, one usually wants a partner who understands
 and speaks that same language. Likely, one wants a whole community, topics
 to talk about, or even a set of shared beliefs or mythologies. This desire
 maps onto the realm of programming languages. When using a particular PL,
 you want to talk to others about your code, implement established design patterns,
 use existing libraries.
 I mentioned mythologies earlier. In some ways, language
 communities do more than share know-how about writing code. In many
 cases, I think language communities rally around ideals embodied by their
 language. The most obvious example seems to be Rust. From what I've seen,
 the Rust community believes in language design that protects its users
 from the pitfalls of low-level programming. The Go community
 believes in radical simplicity. Julia actively incorporates contributions from
 diverse research projects into an interoperable set of scientific packages.
 * __Reason 6__: programming languages are complex collaborative social projects
  that have the power to champion innovative ideas within the field of
  computer science.
 So far, I've presented interpretations of the field of PL as tools for expression and thought,
 human harbor to the universe's ocean, and collaborative social projects.
 These interpretations coexist and superimpose, but they are only a fraction of
 the whole. What has kept me enamored with PL is that it blends these human
 aspects with a mathematical ground truth, through fundamental connections to
 computation and mathematics.
 ### The Mathematics of PL
 > Like buses: you wait two thousand years for a definition of “effectively
 > calculable”, and then three come along at once.
 >
 > --- Philip Wadler, _Propositions as Types_
 There are two foundations,
 [lambda calculus](https://en.wikipedia.org/wiki/Lambda_calculus) and
 [Turing machines](https://en.wikipedia.org/wiki/Turing_machine), that underpin
 most modern PLs. The abstract notion of Turing machines
 is closely related to, and most similar among the "famous" computational models,
 to the
 [von Neumann Architecture](https://en.wikipedia.org/wiki/Von_Neumann_architecture).
 Through bottom-up organization of "control unit instructions" into
 "structured programs" into the imperative high-level languages today, we can
 trace the influence of Turing machines in C++, Python, Java, and many others.
 At the same time, and running on the same hardware functional programming
 languages like Haskell represent a chain of succession from the lambda calculus,
 embellished today with types and numerous other niceties. These two lineages
 are inseparably linked: they have been mathematically proven to be equivalent.
 They are two worlds coexisting.
 The two foundations have a crucial property in common: they are descriptions
 of what can be computed. Both were developed initially as mathematical formalisms.
 They are rooted not only in pragmatic concerns of "what can I do with
 these transistors?", but in the deeper questions of "what can be done
 with a computer?".
 * __Reason 7__: general-purpose programming languages are built on foundations of computation,
  and wield the power to compute anything we consider "effectively computable at all".
 Because of these mathematical beginnings, we have long had precise and powerful
 ways to talk about what code written in a particular language _means_.
 This is the domain of _semantics_. Instead of reference implementations
 of languages (CPython for Python, `rustc` for Rust), and instead of textual
 specifications, we can explicitly map constructs in languages either to
 mathematical objects ([denotational semantics](https://en.wikipedia.org/wiki/Denotational_semantics))
 or to (abstractly) execute them ([operational semantics](https://en.wikipedia.org/wiki/Operational_semantics)).
 To be honest, the precise and mathematical nature of these tools is, for me,
 justification enough to love them. However, precise semantics for languages
 have real advantages. For one, they allow us to compare programs' real
 behavior with what we _expect_, giving us a "ground truth" when trying to
 fix bugs or evolve the language. For another, they allow us to confidently
 make optimizations: if you can _prove_ that a transformation won't affect
 a program's behavior, but make it faster, you can safely use it. Finally,
 the discipline of formalizing programming language semantics usually entails
 boiling them down to their most essential components. Stripping the
 [syntax sugar](https://en.wikipedia.org/wiki/Syntactic_sugar) helps clarify
 how complex combinations of features should behave together.
 Some of these techniques bear a noticeable resemblance to the study of
 semantics in linguistics. Given our preceding discussion on the humanity
 of programming languages, perhaps that's not too surprising.
 * __Reason 8__: programming languages can be precisely formalized, giving
  exact, mathematical descriptions of how they should work.
 In talking about how programs behave, we run into an important limitation
 of reasoning about Turing machines and lambda calculus, stated precisely in
 [Rice's theorem](https://en.wikipedia.org/wiki/Rice%27s_theorem):
 all non-trivial semantic properties of programs (termination, throwing errors)
 are undecidable. There will always be programs that elude not only human analysis,
 but algorithmic understanding.
 It is in the context of this constraint that I like to think about type systems.
 The beauty of type systems, to me, is in how they tame the impossible.
 Depending on the design of a type system, a well-typed program may well be
 guaranteed not to produce any errors, or produce only the "expected" sort of
 errors. By constructing reasonable _approximations_ of program
 behavior, type systems allow us to verify that programs are well-behaved in
 spite of Rice's theorem. Much of the time, too, we can do so in a way that is
 straightforward for humans to understand and machines to execute.
 * __Reason 9__: in the face of the fundamentally impossible, type systems
  pragmatically grant us confidence in our programs for surprisingly little
  conceptual cost.
 At first, type systems look like engineering formalisms. That
 may well be the original intention, but in our invention of type systems,
 we have actually completed a quadrant of a deeper connection: the
 [Curry-Howard isomorphism](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence).
 [Propositions](https://en.wikipedia.org/wiki/Proposition), in the logical sense,
 correspond one-to-one with types of programs, and proofs of these propositions
 correspond to programs that have the matching type.
 This is an incredibly deep connection. In adding parametric polymorphism
 to a type system (think Java generics, or C++ templates without specialization),
 we augment the corresponding logic with the "for all x" (\(\forall x\)) quantifier.
 Restrict the copying of values in a way similar to Rust, and you get an
 [affine logic](https://en.wikipedia.org/wiki/Affine_logic), capable of reasoning about resources and their use.
 In languages like Agda with [dependent types](https://en.wikipedia.org/wiki/Dependent_type),
 you get a system powerful enough [to serve as a foundation for mathematics](https://en.wikipedia.org/wiki/Intuitionistic_type_theory).
 Suddenly, you can write code and mathematically prove properties about that
 code in the same language. I've done this in my work with
 [formally-verified static program analysis]({{< relref "series/static-program-analysis-in-agda" >}}).
 This connection proves appealing even from the perspective of "regular"
 mathematics. We have developed established engineering practices
 for writing code: review, deployment, documentation. What if we could use
 the same techniques for doing mathematics? What if, through the deep
 connection of programming languages to logic, we could turn mathematics
 into a computer-verified, collaborative endeavor?
 I therefore present:
 * __Reason 10__: type systems for programming languages deeply correspond
  to logic, allowing us to mathematically prove properties about code,
  using code, and to advance mathematics through the practices of software engineering.
 {{< details summary="Bonus meta-reason to love the mathy side of PL!" >}}
 In addition to the theoretical depth, I also find great enjoyment in the way that PL is practiced.
 Here more than elsewhere, creativity and artfulness come into
 play. In PL, [inference rules](https://en.wikipedia.org/wiki/Rule_of_inference) are a
 lingua franca through which the formalisms I've mentioned above are expressed
 and shared. They are such a central tool in the field that I've
 developed [a system for exploring them interactively]({{< relref "blog/bergamot" >}})
 on this blog.
 In me personally, inference rules spark joy. They are a concise and elegant
 way to do much of the formal heavy-lifting I described in this section;
 we use them for operational semantics, type systems, and sometimes more.
 When navigating the variety and complexity of the many languages and type
 systems out there, we can count on inference rules to take us directly to
 what we need to know. This same variety naturally demands flexibility in
 how rules are constructed, and what notation is used. Though this can sometimes
 be troublesome (one [paper](https://labs.oracle.com/pls/apex/f?p=LABS%3A0%3A%3AAPPLICATION_PROCESS%3DGETDOC_INLINE%3A%3A%3ADOC_ID%3A959")
 I've seen describes __27__ different ways of writing the simple operation of substitution in literature!),
 it also creates opportunities for novel and elegant ways of formalizing
 PL.
 * __Bonus Reason__: the field of programming languages has a standard technique
  for expressing its formalisms, which precisely highlights core concepts
  and leaves room for creative expression and elegance.
 {{< /details >}}
 I know that mathematics is a polarizing subject. Often, I find myself
 torn between wanting precision and eschewing overzealous formalism. The
 cusp between the two is probably determined by my own tolerance for abstraction.
 Regardless of how much abstraction you are interested in learning about,
 PL has another dimension, close to the ground: more often than not, our languages
 need to execute on real hardware.
 ### Pragmatics of PL
 Your perfectly-designed language can be completely useless if there is no
 way to
 {{< sidenote "right" "execute-note" "execute it" >}}
 Technically, there are language that don't care if you execute them at all.
 Many programs in theorem-proving languages like Agda and Rocq exist only
 to be type-checked. So, you could nitpick this claim; or, you could take
 it more generally: your language can be useless if there's no
 way to make it efficiently do what it's been made to do.
 {{< /sidenote >}} efficiently. Thus, the field of PL subsumes not only
 the theoretical foundations of languages and their human-centric design; it
 includes also their realization as software.
 The overall point of this section is that there is much depth to the techniques
 involved in bringing a programming language to life. If you are a tinkerer
 or engineer at heart, you will never run out of avenues of exploration.
 The reasons are all framed from this perspective.
 One fascinating aspect to programming languages is the "direction" from
 which they have grown. On one side, you have languages that came
 together from the need to control and describe hardware. I'd say that
 this is the case for C and C++, Fortran, and others. More often than not,
 these languages are compiled to machine code. Still subject to human
 constraints, these languages often evolve more user-facing features as time
 goes on. On the other side, you have languages developed to enable
 people to write software, later faced constraints of actually working
 efficiently. These are languages like Python, Ruby, and JavaScript. These
 languages are often interpreted (executed by a dedicated program), with
 techniques such as [just-in-time compilation](https://en.wikipedia.org/wiki/Just-in-time_compilation).
 There is no one-size-fits-all way to execute a language, and as a result,
 * __Reason 11__: the techniques of executing programming languages are varied
  and rich. From compilation, to JIT, to interpretation, the field
  has many sub-disciplines, each with its own know-hows and tricks.
 At the same time, someone whose goal is to actually develop a compiler
 likely doesn't want to develop everything from scratch. To do so would
 be a daunting task, especially if you want the compiler to run beyond
 the confines of a personal machine. CPU [architectures](https://en.wikipedia.org/wiki/Instruction_set_architecture)
 and operating system differences are hard for any individual to keep up with.
 Fortunately, we have a gargantuan ongoing effort in the field:
 the [LLVM Project](https://llvm.org/). LLVM spans numerous architectures
 and targets, and has become a common back-end for languages like C++
 (via [Clang](https://clang.llvm.org/get_started.html)), Swift, and Rust.
 LLVM helps share and distribute the load of keeping up with the ongoing
 march of architectures and OSes. It also provides a shared playground upon
 which to experiment with language implementations, optimizations, and more.
 * __Reason 12__: large projects like LLVM enable language designers to
  lean on decades of precedent to develop a compiler for their language.
 Though LLVM is powerful, it does not automatically grant languages implemented
 with it good performance. In fact, no other tool does. To make a language
 run fast requires a deep understanding of the language itself, the hardware
 upon which it runs, and the tools used to execute it. That is a big ask!
 Modern computers are extraordinarily complex. Techniques such as
 [out-of-order execution](https://en.wikipedia.org/wiki/Out-of-order_execution),
 [caching](https://en.wikipedia.org/wiki/Cache_(computing)#HARDWARE),
 and [speculative execution](https://en.wikipedia.org/wiki/Speculative_execution)
 are constantly at play. This means that any program is subject to hard-to-predict
 and often unintuitive effects. On top of that, depending on your language's
 capabilities, performance work can often entail working with additional
 hardware, such as GPUs and NICs, which have their own distinct performance
 characteristics. This applies both to compiled and interpreted languages.
 Therefore, I give you:
 * __Reason 13__: improving the performance of a programming language is rife
  with opportunities to engage with low-level details of the hardware
  and operating system.
 In the [mathematics section](#the-mathematics-of-pl), we talked about how constructing correct
 optimizations requires an understanding of the language's semantics. It
 was one of the practical uses for having a mathematical definition of a language.
 Reason 13 is where that comes in, but the synthesis is not automatic. In fact,
 a discipline sits in-between defining how a language behaves and
 optimizing programs: program analysis. Algorithms that analyze
 properties of programs such as [reaching definitions](https://en.wikipedia.org/wiki/Reaching_definition)
 enable optimizations such as [loop-invariant code motion](https://en.wikipedia.org/wiki/Loop-invariant_code_motion),
 which can have very significant performance impact. At the same time, for an
 analysis to be correct, it must be grounded in the program's mathematical
 semantics. There are many fascinating techniques in this discipline,
 including [ones that use lattice theory](https://cs.au.dk/~amoeller/spa/spa.pdf).
 * __Reason 14__: the sub-discipline of program analysis serves as a grounded
  application of PL theory to PL practice, enabling numerous optimizations
  and transformations.
 The programs your compiler generates are software, and, as we just saw,
 may need to be tweaked for performance. But the compiler and/or interpreter
 is itself a piece of software, and its own performance. Today's language
 implementations are subject to demands that hadn't been there historically.
 For instance, languages are used to provide [language servers](https://microsoft.github.io/language-server-protocol/)
 to enable editors to give users deeper insights into their code. Today,
 a language implementation may be called upon every keystroke to provide
 a typing user live updates. This has led to the introduction of
 techniques like the [query architecture](https://ollef.github.io/blog/posts/query-based-compilers.html)
 (see also [salsa](https://github.com/salsa-rs/salsa)) to avoid
 redundant work and re-used intermediate results. New language implementations
 like that of [Carbon](https://github.com/carbon-language/carbon-lang)
 are exploring alternative representations of programs in memory. In
 short,
 * __Reason 15__: language implementations are themselves pieces of software,
  subject to unique constraints and requiring careful and innovative
  engineering.
 ### Conclusion
 I've now given a tour of ways in which I found the PL field compelling,
 organized across three broad categories. There is just one more reason
 I'd like to share.
 I was 16 years old when I got involved with the world of programming
 languages and compilers. Though I made efforts to learn about it through
 literature (the _Dragon Book_, and _Modern Compiler Design_), I simply
 didn't have the background to find these resources accessible. However, all
 was not lost. The PL community online has been, and still is, a vibrant and
 enthusiastic place. I have found it to be welcoming of folks with backgrounds
 spanning complete beginners and experts alike. Back then, it gave me
 accessible introductions to anything I wanted. Now, every week I see new
 articles go by that challenge my intuitions, teach me new things, or take PL
 ideas to absurd and humorous extremes. So, my final reason:
 * __Reason 16__: the programming languages community is full of brilliant,
  kind, welcoming and enthusiastic people, who dedicate much of their
  time to spreading the joy of the field.
  I ❤️ the programming languages community.
--- a/content/blog/idris_catamorphisms.md
+++ b/content/blog/idris_catamorphisms.md
@@ -17,7 +17,8 @@ spend time explaining dependent types, nor the syntax for them in Idris,
 which is the language I'll use in this article. Below are a few resources
 that should help you get up to speed.
-{{< todo >}}List resources{{< /todo >}}
+> [!TODO]
 > List resources
 We've seen that, given a function `F a -> a`, we can define a function
 `B -> a`, if `F` is a base functor of the type `B`. However, what if
--- a/content/blog/introducing_highlight/thumbnail.png
+++ b/content/blog/introducing_highlight/thumbnail.png
--- a/content/blog/llm_personal_software/index.md
+++ b/content/blog/llm_personal_software/index.md
@@ -0,0 +1,190 @@
 ---
 title: "Personal Software with the Help of LLMs"
 date: 2026-04-05T16:03:00-07:00
 tags: ["LLMs"]
 series: ["LLM-Assisted Flashcard Generator"]
 description: "In this post, I describe an inherently individual and outcome-focused class of LLM-generated software"
 ---
 In [the previous post in this series]({{< relref "pdf_flashcards_llm" >}}),
 I wrote about a little utility I created for detecting underlined words
 in a book and creating vocabulary study material for them.
 Like I mentioned earlier, this was one of my earliest experiences with
 LLM-driven development, and I think it shaped my outlook on the technology
 quite a bit. For me, the bottom line is this: _with LLMs, I was able to
 rapidly solve a problem that was holding me back in another area of my life_.
 My goal was never to "produce software", but to "acquire vocabulary",
 and, viewed from this perspective, I think the experience has been a
 colossal success.
 As someone who works on software, I am always reminded that end-users rarely
 care about the technology as much as we technologists; they care about
 having their problems solved. I find taking that perspective to be challenging
 (though valuable) because software is my craft, and because in thinking
 about the solution, I have to think about the elements that bring it to life.
 With LLMs, I was able --- allowed? --- to view things more from the
 end-user perspective. I didn't know, and didn't need to know, the API
 for `PyMuPDF`, `argostranslate`, or `spaCy`. I didn't need to understand
 the PDF format. I could move one step away from the nitty-gritty and focus
 on the 'why' and the 'what', on the challenge of what I wanted to accomplish.
 I wrestled with the inherent complexity and
 avoided altogether the unrelated difficulties that merely happened to be
 there (downloading language modules; learning translation APIs; etc.)
 By enabling me to do this, the LLM let me make rapid progress, and to produce
 solutions to problems I would've previously deemed "too hard" or "too tedious".
 This did, however, markedly reduce the care with which I was examining
 the output. I don't think I've _ever_ read the code that produces the
 pretty colored boxes in my program's debug output. This shift, I think,
 has been a divisive element of AI discourse in technical communities.
 I think that this has to do, at least in part, with different views
 on code as a medium.
 #### The Builders and the Craftsmen
 There are two perspectives through which one may view software:
 as a craft in and of itself, and as a means to some end.
 My flashcard extractor can be viewed in vastly different ways when faced
 from these two perspectives. In terms of craft, I think that it is at best
 mediocre; most of the code is generated, slightly verbose and somewhat
 tedious. The codebase is far from inspiring, and if I had written it by hand,
 I would not be particularly proud of it. In terms of product, though,
 I think it tells an exciting story: here I am, reading Camus again, because
 I was able to improve the workflow around said reading. In a day, I was able
 to achieve what I couldn't muster in a year or two on my own.
 The truth is, the "builder vs. craftsman" distinction is a simplifying one,
 another in the long line of "us vs. them" classifications. Any one person is
 capable of being any combination of these two camps at any given time. Indeed,
 different sorts of software demand to be viewed through different lenses.
 I will _still_ treat work on my long-term projects as a craft, because
 I will come back to it again and again, and because our craft has evolved
 to engender stability and maintainability.
 However, I am more than happy to settle for 'underwhelming' when it means an
 individual need of mine can be addressed in record time. I think this
 gives rise to a new sort of software: highly individual, explicitly
 non-robust, and treated differently from software crafted with
 deliberate thought and foresight.
 #### Personal Software
 I think as time goes on, I am becoming more and more convinced by the idea
 of "personal software". One might argue that much of the complexity in many
 pieces of software is driven by the need of that software to accommodate
 the diverse needs of many users. Still, software remains somewhat inflexible and
 unable to accommodate individual needs. Features or uses that demand
 changes at the software level move at a slower pace: finite developer time
 needs to be spent analyzing what users need, determining the costs of this new
 functionality, choosing which of the many possible requests to fulfill.
 On the other hand, software that enables the users to build their customizations
 for themselves, by exposing numerous configuration options and abstractions,
 becomes, over time, very complicated to grasp.
 Now, suppose that the complexity of such software scales superlinearly with
 the number of features it provides. Suppose also that individual users
 leverage only a small subset of the software's functionality. From these
 assumptions it would follow that individual programs, made to serve a single
 user's need, would be significantly less complicated than the "whole".
 By definition, these programs would also be better tailored to the users'
 needs. With LLMs, we're getting to a future where this might be possible.
 I think that my flashcard generator is an early instance of such software.
 It doesn't worry about various book formats, or various languages, or
 various page layouts. The heuristic was tweaked to fit my use case, and
 now works 100% of the time. I understand the software in its entirety.
 I thought about sharing it --- and, in a way, I did, since it's
 [open source](https://dev.danilafe.com/DanilaFe/vocab-builder) --- but realized
 that outside of the constraints of my own problem, it likely will not be
 of that much use. I _could_ experiment with more varied constraints, but
 that would turn it back into the sort of software I discussed above:
 general, robust, and complex.
 Today, I think that there is a whole class of software that is amenable to
 being "personal". My flashcard generator is one such piece of software;
 I imagine file-organization (as served by many "bulk rename and move" pieces
 of software out there), video wrangling (possible today with `ffmpeg`'s
 myriad of flags and switches), and data visualization to be other
 instances of problems in that class. I am merely intuiting here, but
 if I had to give a rough heuristic, it would be problems that:
 * __fulfill a short-frequency need__, because availability, deployment,
  etc. significantly raises the bar for quality.
  * e.g., I collect flashcards once every two weeks;
    I organize my filesystem once a month; I don't spend nearly enough money
    to want to regenerate cash flow charts very often
 * __have an "answer" that's relatively easy to assess__, because
  LLMs are not perfect and iteration must be possible and easy.
  * e.g., I can see that all the underlined words are listed in my web app;
    I know that my files are in the right folders, named appropriately,
    by inspection; my charts seem to track with reality
 * __have a relatively complex technical implementation__, because
  why would you bother invoking an LLM if you can "just" click a button somewhere?
  * e.g., extracting data from PDFs requires some wrangling;
    bulk-renaming files requires some tedious and possibly case-specific
    pattern matching; cash flow between N accounts requires some graph
    analysis
 * __have relatively low stakes__, again, because LLMs are not perfect,
  and nor is (necessarily) one's understanding of the problem.
  * e.g., it's OK if I miss some words I underlined; my cash flow
    charts only give me an impression of my spending;
  * I recognize that moving files is a potentially destructive operation.
 I dream of a world in which, to make use of my hardware, I just _ask_,
 and don't worry much about languages, frameworks, or sharing my solution
 with others --- that last one because they can just ask as well.
 #### The Unfair Advantage of Being Technical
 I recognize that my success described here did not come for free. There
 were numerous parts of the process where my software background helped
 me get the most out of Codex.
 For one thing, writing software trains us to think precisely about problems.
 We learn to state exactly what we want, to decompose tasks into steps,
 and to intuit the exact size of these steps; to know what's hard and what's
 easy for the machine. When working with an LLM, these skills make it possible
 to hit the ground running, to know what to ask and to help pluck out a particular
 solution from the space of various approaches. I think that this greatly
 accelerates the effectiveness of using LLMs compared to non-technical experts.
 For another, the boundary between 'manual' and 'automatic' is not always consistent.
 Though I didn't touch any of the `PyMuPDF` code, I did need to look fairly
 closely at the logic that classified my squiggles as "underlines" and found
 associated words. It was not enough to treat LLM-generated code as a black box.
 Another advantage software folks have when leveraging LLMs is the established
 rigor of software development. LLMs can and do make mistakes, but so do people.
 Our field has been built around reducing these mistakes' impact and frequency.
 Knowing to use version control helps turn the pathological downward spiral
 of accumulating incorrect tweaks into monotonic, step-wise improvements.
 Knowing how to construct a test suite and thinking about edge cases can
 provide an agent LLM the grounding it needs to iterate rapidly and safely.
 In this way, I think the dream of personal software is far from being realized
 for the general public. Without the foundation of experience and rigor,
 LLM-driven development can easily devolve into a frustrating and endless
 back-and-forth, or worse, successfully build software that is subtly and
 convincingly wrong.
 #### The Shoulders of Giants
 The only reason all of this was possible is that the authors of `PyMuPDF`,
 `genanki`, `spaCy`, and `argos-translate` made them available for me to use from
 my code. These libraries provided the bulk of the functionality that Codex and I
 were able to glue into a final product. It would be a mistake to forget this,
 and to confuse the sustained, thoughtful efforts of the people behind these
 projects for the one-off, hyper-specific software I've been talking about.
 We need these packages, and others like them, to provide a foundation for the
 things we build. They bring stability, reuse, and the sort of cohesion that
 is not possible through an amalgamation of home-grown personal scripts.
 In my view, something like `spaCy` is to my flashcard script as a brick is to
 grout. There is a fundamental difference.
 I don't know how LLMs will integrate into the future of large-scale software
 development. The discipline becomes something else entirely when the
 constraints of "personal software" I floated above cease to apply. Though
 LLMs can still enable doing what was previously too difficult, tedious,
 or time consuming (like my little 'underline visualizer'), it remains
 to be seen how to integrate this new ease into the software lifecycle
 without threatening its future.
--- a/content/blog/modulo_patterns/thumbnail.png
+++ b/content/blog/modulo_patterns/thumbnail.png
--- a/content/blog/pdf_flashcards_llm/flaggedmarks.png
+++ b/content/blog/pdf_flashcards_llm/flaggedmarks.png
--- a/content/blog/pdf_flashcards_llm/index.md
+++ b/content/blog/pdf_flashcards_llm/index.md
@@ -0,0 +1,239 @@
 ---
 title: "Generating Flashcards from PDF Underlines"
 date: 2026-04-05T16:02:00-07:00
 tags: ["LLMs", "Python"]
 series: ["LLM-Assisted Flashcard Generator"]
 description: "In this post, I describe my personal PDF-to-vocab-flashcards pipeline"
 ---
 __TL;DR__: I, with the help of ChatGPT, wrote [a program](https://dev.danilafe.com/DanilaFe/vocab-builder)
 that helps me extract vocabulary words from PDFs. Scroll just a bit further down
 to see what it looks like.
 Sometime in 2020 or 2021, during the COVID-19 pandemic, I overheard from some
 source that Albert Camus, in his book _La Peste_ (The Plague), had quite
 accurately described the experience that many of us were going through
 at the time. Having studied French for several years, I decided that the
 best way to see for myself what _La Peste_ is all about was to read it
 in its original, untranslated form.
 I made good progress, but I certainly did not know every word. At the surface,
 I was faced with two choices: guess the words from context and read without
 stopping, or interrupt my reading to look up unfamiliar terms. The former
 seemed unfortunate since it stunted my ability to acquire new vocabulary;
 the latter was unpleasant, making me constantly break from the prose
 (and the e-ink screen of my tablet) to consult a dictionary.
 In the end, I decided to underline the words, and come back to them later.
 However, even then, the task is fairly arduous. For one, words I don't recognize
 aren't always in their canonical form (they can be conjugated, plural, compound,
 and more): I have to spend some time deciphering what I should add to a
 flashcard. For another, I had to bounce between a PDF of my book
 (from where, fortunately, I can copy-paste) and my computer. Often, a word
 confused the translation software out of context, so I had to copy more of the
 surrounding text. Finally, I learned that given these limitations, the pace of
 my reading far exceeds the rate of my translation. This led me to underline
 fewer words.
 I thought,
 > Perhaps I can just have some software automatically extract the underlined
 > portions of the words, find the canonical forms, and generate flashcards?
 Even thinking this thought was a mistake. From then on, as I read and went
 about underlining my words, I thought about how much manual effort I will
 be taking on that could be automated. However, I didn't know how to start
 the automation. In the end, I switched to reading books in English.
 Then, LLMs got good at writing code. With the help of
 Codex, I finally got the tools that I was dreaming about. Here's what it looks
 like.
 {{< figure src="./underlines.png" caption="Detected underlined words on a page" label="Detected underlined words on a page" >}}
 {{< figure src="./result.png" caption="Auto-flashcard application" label="Auto-flashcard application" class="fullwide" >}}
 This was my first foray into LLM-driven development. My commentary about that
 experience (as if there isn't enough of such content out there!) will be
 interleaved with the technical details.
 ### The Core Solution
 The core idea has always been:
 1. Find things that look like underlines
 2. See which words they correspond to
 3. Perform {{< sidenote "right" "lemmatization-node" "lemmatization" >}}
 Lemmatization (<a href="https://en.wikipedia.org/wiki/Lemmatization">Wikipedia</a>) is the
 process of turning non-canonical forms of words (like <code>am</code> (eng) /
 <code>suis</code> (fr)) into their canonical form which might be found in the
 dictionary (<code>to be</code> / <code>être</code>).
 {{< /sidenote >}} and translate.
 My initial direction was shaped by the impressive demonstrations of OCR
 models, which could follow instructions at the same time as reading a document.
 For these models, a prompt like "extract all the text in the red box"
 constituted the entire targeted OCR pipeline. My hope was that a similar
 prompt, "extract all underlined words", would be sufficient to accomplish
 steps 1 and 2. However, I was never to find out: as it turns out,
 OCR models are large and very expensive to run. In addition, the model
 that I was looking at was specifically tailored for NVIDIA hardware which
 I, with my MacBook, simply didn't have access to.
 In the end, I came to the conclusion that a VLM is overkill for the problem
 I'm tackling. This took me down the route of analyzing the PDFs. The
 problem, of course, is that I know nothing of the Python landscape
 of PDF analysis tools, and that I also know nothing about the PDF format
 itself. This is where a Codex v1 came in. Codex opted (from its training
 data, I presume) to use the [`PyMuPDF`](https://pymupdf.readthedocs.io) package.
 It also guessed (correctly) that the PDFs exported by my tablet used
 the 'drawings' part of the PDF spec to encode what I penned. I was instantly
 able to see (on the console) the individual drawings.
 The LLM also chose to approach the problem by treating each drawing as just
 a "cloud of points", discarding the individual line segment data. This
 seemed like a nice enough simplification, and it worked well in the long run.
 #### Iterating on the Heuristic
 The trouble with the LLM agent was that it had no good way of verifying
 whether the lines it detected (and indeed, the words it considered underlined)
 were actually lines (and underlined words). Its initial algorithm missed
 many words, and misidentified others. I had to resort to visual inspection
 to see what was being missed, and for the likely cause.
 The exact process of the iteration is not particularly interesting. I'd
 tweak a threshold, re-run the code, and see the new list of words.
 I'd then cross-reference the list with the page in question, to see
 if things were being over- or under-included. Rinse, repeat.
 This got tedious fast. In some cases, letters or words I penned would get picked
 up as underlines, and slightly diagonal strokes would get missed. I ended up
 requesting Codex to generate a debugging utility that highlighted (in a box)
 all the segments that it flagged, and the corresponding words. This
 is the first picture I showed in the post. Here it is again:
 {{< figure src="./underlines.png" caption="Detected underlined words on a page" label="Detected underlined words on a page" >}}
 In the end, the rough algorithm was as follows:
 1. __Identify all "cloud points" that are not too tall__. Lines that
   vertically span too many lines of text are likely not underlines.
   * The 'height threshold' ended up being larger than I anticipated:
     turns out I don't draw very straight horizontal lines.
     {{< figure src="tallmarks.png" caption="My angled underlines" label="My angled underlines" >}}
 2. __Create a bounding box for the line,__ with some padding.
   I don't draw the lines _directly_ underneath the text, but a bit below.
   * Sometimes, I draw the line quite a bit below; the upward padding
     had to be sizeable.
     {{< figure src="lowmarks.png" caption="My too-low underlines" label="My too-low underlines" >}}
 3. __Intersect `PyMuPDF` bounding boxes with the line__. Fortunately,
   `PyMuPDF` provides word rectangles out of the box.
   * I required the intersection to overlap with at least 60% of the word's
     horizontal width, so accidental overlaps don't count.
     {{< figure src="widemarks.png" caption="My too-wide underline hitting `Cela`" label="My too-wide underline hitting `Cela`" >}}
   * The smallest underlines are roughly the same size as the biggest strokes
     in my handwriting. The 60% requirement filtered out the latter, while
     keeping the former.
     {{< figure src="flaggedmarks.png" caption="Letters of a hand-writing word detected as lines" label="Letters of a hand-writing word detected as lines" >}}
 4. __Reject underlines that overlap from the top__. Since, as I mentioned,
   my underlines are often so low that they touch the next line.
 #### Lemmatization and Translation
 I don't recall now how I arrived at [`spaCy`](https://github.com/explosion/spaCy),
 but that's what I ended up using for my lemmatization. There was only
 one main catch: sometimes, instead of underlining words I didn't know,
 I underlined whole phrases. Lemmatization did not work well in those
 contexts; I had to specifically restrict my lemmatization to single-word
 underlines, and to strip punctuation which occasionally got tacked on.
 With lemmatization in hand, I moved on to the next step: translation.
 I wanted my entire tool to work completely offline. As a result, I had to
 search for "python offline translation", to learn about
 [`argos-translate`](https://github.com/argosopentech/argos-translate).
 Frankly, the translation piece is almost entirely uninteresting:
 it boils down to invoking a single function. I might add that
 `argos-translate` requires one to download language packages --- they
 do not ship with the Python package. Codex knew to write a script to do
 so, which saved a little bit of documentation-reading and typing.
 The net result is a program that could produce:
 ```
 Page 95: fougueuse -> fougueux -> fiery
 ```
 Pretty good!
 ### Manual Intervention
 That "pretty good" breaks down very fast. There are several points of failure:
 the lemmatization can often get confused, and the offline translation
 fails for some of the more flowery Camus language.
 In the end, for somewhere on the order of 70% of the words I underlined,
 the automatic translation was insufficient, and required small tweaks
 (changing the tense of the lemma, adding "to" to infinitive English verbs, etc.)
 I thought --- why not just make this interactive? Fortunately, there are
 plenty of Flask applications in Codex's training dataset. In one shot,
 it generated a little web application that enabled me to tweak the source word
 and final translation. It also enabled me to throw away certain underlines.
 This was useful when, across different sessions, I forgot and underlined
 the same word, or when I underlined a word but later decided it was not worth
 including in my studying. This application produced an Anki deck, using
 the Python library [`genanki`](https://github.com/kerrickstaley/genanki).
 Anki has a nice mechanism to de-duplicate decks, which meant that every
 time I exported a new batch of words, I could add them to my running
 collection.
 Even then, however, cleaning up the auto-translation was not always easy.
 The OCR copy of the book had strange idiosyncrasies: the letters 'fi' together
 would OCR to '=' or '/'. Sometimes, I would underline a compound phrase
 that spanned two lines; though I knew the individual words (and would be surprised
 to find them in my list), I did not know their interaction.
 In the end, I added (had Codex add) both a text-based context and a visual
 capture of the word in question to the web application. This led to the final
 version, whose screenshot I included above. Here it is again:
 {{< figure src="./result.png" caption="Auto-flashcard application" label="Auto-flashcard application" class="fullwide" >}}
 The net result was that, for many words, I could naively accept the
 automatically-generated suggestion. For those where this was not possible,
 in most cases I only had to tweak a few letters, which still saved me time.
 Finally, I was able to automatically include the context of the word in
 my flashcards, which often helps reinforce the translation and remember
 the exact sense in which the word was used.
 To this day, I haven't found a single word that was underlined and missed,
 nor one that was mis-identified as underlined.
 ### Future Direction
 In many ways, this software is more than good enough for my needs.
 I add a new batch of vocabulary roughly every two weeks, during which time
 I manually export a PDF of _La Peste_ from my tablet and plug it into
 my software.
 In my ideal world, I wouldn't have to do that. I would just underline some
 words, and come back to my laptop a few days later to find a set of draft
 flashcards for me to review and edit. In an even more ideal world, words
 I underline get "magically" translated, and the translations appear somewhere
 in the margins of my text (while also being placed in my list of flashcards).
 I suspect LLMs --- local ones --- might be a decent alternative technology
 to "conventional" translation. By automatically feeding them the context
 and underlined portion, it might be possible to automatically get a more
 robust translation and flashcard. I experimented with this briefly
 early on, but did not have much success. Perhaps better prompting or newer
 models would improve the outcomes.
 That said, I think that those features are way beyond the 80:20 transition:
 it would be much harder for me to get to that point, and the benefit would
 be relatively small. Today, I'm happy to stick with what I already have.
 In the [next part of this series]({{< relref "llm_personal_software" >}}),
 I will talk more about how this project influenced my views on LLMs.
--- a/content/blog/pdf_flashcards_llm/lowmarks.png
+++ b/content/blog/pdf_flashcards_llm/lowmarks.png
--- a/content/blog/pdf_flashcards_llm/result.png
+++ b/content/blog/pdf_flashcards_llm/result.png
--- a/content/blog/pdf_flashcards_llm/tallmarks.png
+++ b/content/blog/pdf_flashcards_llm/tallmarks.png
--- a/content/blog/pdf_flashcards_llm/thumbnail.png
+++ b/content/blog/pdf_flashcards_llm/thumbnail.png
--- a/content/blog/pdf_flashcards_llm/underlines.png
+++ b/content/blog/pdf_flashcards_llm/underlines.png
--- a/content/blog/pdf_flashcards_llm/widemarks.png
+++ b/content/blog/pdf_flashcards_llm/widemarks.png
--- a/content/series/llm-assisted-flashcard-generator/_index.md
+++ b/content/series/llm-assisted-flashcard-generator/_index.md
@@ -0,0 +1,11 @@
 +++
 title = "LLM-Assisted Flashcard Generator"
 summary = """
  In this series, I write up a little program I wrote for myself,
  which detects vocabulary words I underline in a book and turns them
  into flashcards. I view this through the lens of a first foray into
  development that heavily relies on LLMs.
  """
 status = "complete"
 donotunique = true
 +++
--- a/content/series/static-program-analysis-in-agda/_index.md
+++ b/content/series/static-program-analysis-in-agda/_index.md
@@ -6,6 +6,6 @@ summary = """
  in Agda. The goal is to have a formally verified, yet executable, static
  analyzer for a simple language.
  """
-status = "ongoing"
+status = "complete"
 divider = ": "
 +++
--- a/content/writing/onspiders/index.md
+++ b/content/writing/onspiders/index.md
@@ -0,0 +1,47 @@
 ---
 title: "On Spiders"
 date: 2026-03-22T01:03:00-05:00
 description: "Whenever I stay still, I feel the spiders weave their webs around me."
 custom_css:
 - style.scss
 body_start_partial: "spiderweb.html"
 ---
 ```
 Whenever I stay still,
  I feel the spiders weave their webs around me.
  Their tiny legs entangle me in silk,
  traverse my body as they seem to proudly
  inspect their work and into darkness sink.
  There're times I see the spiders' threads on others,
  They shimmer gently in the purple dusk,
  Or sway with zephyrs in the hair of lovers,
  stuck.
  To listen to the webs is to hear echoes
  of social butterflies ensnared within
  arachnid galleries of human ethos,
  whose pieces come and go upon a whim.
  Their curators are blind and want for stories,
  delivered as vibrations through the links,
  for righteous anger, anguish, joy and worries,
  superimposing frequencies that mix,
  reveberating through the sprawling complex
  of radial lines and newly captured prey,
  resisting first but ultimately hopeless,
  these signals grow in urgency and they
  form standing waves that make the victims sing
  and even from myself bring out a resonant ring.
 ```
 <!--
  the signals cause a standing wave
  intensify with every passing moment
  arachnid galleries of human drama,
  temples to the human mind
  (traverse my body all while I sleep soundly,)
  They shimmer gently in the setting sun, -->
--- a/content/writing/onspiders/style.scss
+++ b/content/writing/onspiders/style.scss
@@ -0,0 +1,19 @@
@import "variables.scss";
@import "mixins.scss";
 .spiderweb {
  position: fixed;
  top: 0;
  right: 0;
  opacity: 0.25;
  max-width: 900px;
  @include below-container-width {
    width: $container-width-threshold;
  }
 }
 code {
  background: none;
  border: none;
 }
--- a/content/writing/pynchon/index.md
+++ b/content/writing/pynchon/index.md
@@ -0,0 +1,144 @@
 ---
 title: "Everything's Touch"
 date: 2026-05-14T18:01:27-07:00
 draft: true
 custom_css:
 - style.scss
 ---
 {{< halfpage >}}
 ## Everything's Touch
 "Do you guys have any deuterium water?", he said to a baffled lab manager.
 "You know, heavy water?"
 "No... We don't have that...". She didn't recognize him as a student.
 "Do you know where I can get some?", continued his barrage of questions,
 "What's a good chemical company? How do I go about ordering heavy water from them?"
 What could this guy possibly have to do with heavy water? Why is he so determined?
 When he finally turned and left empty-handed, she breathed a sigh of relief.
 Until, that is, another man arrived and made the same request: he wanted heavy water.
 Again, the lab manager refused him. For the rest of the day, she had
 a knot in her stomach. Having failed once, in order to remain under the radar,
 had some shadowy cabal switched representatives, and tried again to attain
 their goal?
 Uneasy still the lab manager had dinner, opening YouTube™ on her phone to pass
 the time. On the front page, a video was waiting for her: "the ice cube
 is too heavy!". When frozen, you see, heavy water sinks instead of floating.
 There was no plot. Two men, having both seen this video, had independently
 decided to replicate the trick. On the same day, believing it was their
 free will, they visited the same lab and spoke to the same lab manager.
 They felt the touch.
 ---
 > Roland too became conscious of the wind, as his mortality had never allowed him.
 > Discovered it so. ...so joyful, that the arrow must veer into it.
 >
 > -- Thomas Pynchon, *Gravity's Rainbow*
 Today, we live amidst an invisible ocean, but not in a physical sense;
 its tides don't pull us out to sea or push us towards the shore; no
 warm undercurrents alternate with cool water as we bob in the waves.
 Standing on a hiking trail and looking out at the path ahead, the world
 might look exactly as it had forty years ago. However, the ocean is
 there, mediated by
 {{< /halfpage >}}
 {{< halfpage >}}
 electromagnetism instead of fluid. Looking up at the sky,
 nowadays we are reminded of this by the numerous hurtling dots delivering
 the internet to practically every corner of the planet.
 Reminded are we of its existence, too, when we hear it speak; when people talk
 about Geese and Velvet Underground; when friends repeat nearly verbatim the
 top post on /r/bald; when men show up to a teaching lab and ask for deuterium.
 Sometimes, these ideas are deliberately planted. Sometimes, they are analogous
 to your classic trends™. Sometimes, they just appear. An enormous behemoth
 stirs deep beneath the waves, and we sway with the current.
 ---
 > If it is in working order, what is it meant to do? The engineers
 > who built it . . . never knew there were any further steps to be taken.
 > Their design was "finalized", and they could forget it.
 >
 > -- Thomas Pynchon, *Gravity's Rainbow*
 In _The Age of Surveillance Capitalism_, Shoshana Zuboff
 powerfully reframes the actions of tech giants like Google
 from the perspective of _behavioral surplus_. Google
 and Meta's gluttony for traffic patterns, written sentiment, satellite data,
 identified faces seen by smart glasses, all of it is the endless hunger of an
 influence-machine. Zuboff decries the "priests of the shadow texts",
 Skinnerian manipulators bent on seizing human agency for utopian or,
 more likely, capitalistic ends.
 I don't think that's the whole picture.
 The surveillance-manipulation machine, running at incredible scale and
 nudging us every moment we search or share or scroll, is ultimately
 unconcerned with truth. Truth is secondary to human behavior. While it
 reaches and connects a double-digit percentage of the world's population,
 the machine lacks any constraint or fundamental purpose beyond engagement.
 It's driven by unfathomably large probabilistic models entangled through
 several orders of interactions with other models.
 This enormous amalgamation, joined nowadays by (probably) well-intentioned
 and only-moderately-grounded-in-reality AI™ agents™, is armed with state-of-the-art
 tools and unprecedented influence. With "engagement" its only loose target,
 it ceaselessly perturbs our daily thoughts like Maxwell's demon. Whole
 cliques of people revisit old shows, "discover" a new band, and try Science™.
 {{< /halfpage >}}
 {{< halfpage >}}
 ---
 Among _Gravity's Rainbow_'s
 numerous subjects and themes is an intricate and densely
 connected network of markets, influences, and hidden agendas that overlays
 the political conflicts of World War 2. Individuals pursued their own economic
 gains; dealers replaced cocaine with powdered milk; Phoebus intentionally limited
 the lifetimes of lightbulbs; a man dressed like a Rocket smuggled hash past
 an international gathering on behalf of one Sour Bummer. All of this, though, the whole system, took
 on the life of its own: it was the Rocket-state. It acted in ways that were
 inscrutable, mysterious, and yet behind which, in moments of panic or paranoia,
 one could suspect intent. 
 The Rocket-state, as Pynchon described it, may or may not have existed.
 It certainly does not exist today. However, beyond Zuboff's cycle of
 dispossession, beyond the powerful surveillance state exposed by Snowden,
 today lies the Attention-state. It is the entity stirring occasionally under
 the surface of the internet's ocean.
 I think this is the missing piece. Yes, Google and Meta are selling your
 Gmail inbox's contents to the highest bidder. Yes, the US government is
 in on this. Yeah, Meta's Ray-Bans™ are going to be cataloguing every face
 you encounter on the street, and yeah, the age verification laws are probably
 going to be used to further associate your identity with the rest of
 your data point-cloud. But these are just glimpses of the larger system.
 Those "priests of the shadow texts" are like GR's Freemasons: they perform
 the rituals, but the magic is elsewhere.
 This is the closest we've ever been to a truly "unified consciousness".
 We've built ourselves a noosphere, but it's not what we thought it would
 be. It's not _just_ the "world at our fingertips".
 It's not entirely a reflection of human minds. There is an impurity,
 an additional active force that decides which whispers are carried across
 the ocean and which shouts succumb to the inverse-square law.
 There it sits, this impurity, mixed in with most human knowledge, with the
 immediate awareness of nearly every event as it occurs in most of the developed
 world. It coats our facts like film, and when an acquaintance hands you
 his packaged opinion, it remains in his handprints, and your heart sinks
 like deuterium ice.
 {{< /halfpage >}}
--- a/content/writing/pynchon/style.scss
+++ b/content/writing/pynchon/style.scss
@@ -0,0 +1,93 @@
@import "variables.scss";
@import "margin.scss";
 body {
  text-align: left;
  background-color: white;
  color: black;
  /* reset to light mode */
  @each $varName, $varDefault in $css-vars {
      --#{$varName}: #{$varDefault};
  }
 }
 h1, h2, h3, h4, h5, h6 {
  font-family: "Times New Roman"
 }
 h2 {
  font-size: 18pt;
  margin-bottom: 0.2in;
 }
 .warning {
  max-width: $container-width;
 }
 .halfpage {
  width: 5.5in;
  height: 8.5in;
  padding: 0.25in;
  box-sizing: border-box;
  border: $standard-border;
  flex-shrink: 0;
  margin: 0.25in;
  h2 {
    display: block;
  }
  @media screen and (max-width: 5.5in) {
    width: auto;
    height: auto;
    margin: 0;
    border-left: none;
    border-right: none;
  }
 }
 p {
  margin-top: 0;
  margin-bottom: 0.1in;
 }
 html .container {
  max-width: 12in;
  position: static;
  &:not(main) {
    @include below-two-margins {
      padding: 0 $container-min-padding 0 $container-min-padding;
    }
  }
 }
 main.container {
  font-family: "Times New Roman";
  font-size: 12pt;
  line-height: 14pt;
  display: flex;
  box-sizing: border-box;
  flex-wrap: wrap;
  justify-content: left;
  & > h2 {
    display: none; /* copied title is on the page */
  }
  @media screen and (max-width: 5.5in) {
    display: block;
  }
  @media screen and (max-width: 12in) {
    justify-content: center;
  }
 }
 hr {
  padding-top: 0.1in;
  padding-bottom: 0.1in;
  line-height: 0.1in;
 }
--- a/content/writing/spirits/index.md
+++ b/content/writing/spirits/index.md
@@ -0,0 +1,207 @@
 ---
 title: "Persistence of Vision"
 date: 2026-04-18T23:26:00-07:00
 description: "Humid air swirls with colorful spirits."
 custom_css:
 - style.scss
 ---
 Humid air swirls with colorful spirits. They trace its invisible currents
 in spirals through open spaces, cling to branches, drip down stone faces
 and, awakened by the first beams of the rising sun, ooze newly out of trees
 like sap. Lulls of wind leave them gliding gently downward to be picked up
 again. From a distance, eddies of the spirits' malleable confetti travel
 along plains. With translucent jellylike hands and fingers they wave at
 each other in passing or hold each other in breeze-perturbed waltzes. Big
 luminescent white eyes take in with wonder and awe the only day they are
 ever to see.
 Among them, Hex. An exception within the colorful milieu, he remembers, if
 vaguely, the mornings that precede this one. He feels an unbroken thread
 of identity dissolved somewhere within his red-pink body.
 Spirits disappear at
 dusk, bursting like soap bubbles while the last rays of the setting sun
 still caress from behind horizon-clouds the darkening sky. They are born
 each day, leaping with passing fish out of streams and accumulating in
 drops of dew. An apple doesn't fall far from the tree, and a spirit from
 its genitive landscape. Again and again Hex encounters similar motifs.
 Take Molly, who hangs now with Hex from a grapevine, the both of them agitated
 by the wind resembling pennants on some carnival string. The
 first Molly he met, who serves now for him as a departure point for a whole
 lineage of kindred spirits, was a deep red: she was born during a Fire.
 That day, overburdened clouds covered the sky like dense wool and
 unleashed after much unwanted loitering their promised downpour and
 lightning. Flames spread quickly through the birch forest beneath. The
 Fire raged for days, sucking in the surrounding atmosphere its gluttony
 and spewing it upwards mingled with ash. A haze of purple, pink, orange
 and yellow replaced the thunderclouds.
 Hex was swept then by the Fire's incessant breath towards the birches.
 Flames danced among charred silhouettes that used to be trees.
 A great many spirits were being born, sizzling out of ember-glowing
 stumps and erupting in geysers above the flickering dance to drift upwards
 like hot-air balloons. Molly was among them.
 They sat together on a ledge. His pink hand held hers. By some trick of
 their geometry, the surrounding cliffs gave them refuge from the wind. Hex
 sensed for what felt like the first time the weight of his body, a sort of
 agency. He wanted Molly to understand. He kept stumbling, espousing one
 flawed analogy after another, sketches of a painting that he didn't know
 how to finish, unable to get across the _feeling_, no, "comfort" isn't
 quite right, nor is "boldness", nor... She might have vaguely understood.
 Molly herself wanted weightlessness; he saw the spark in
 her eye when she talked of waking up in the arms of a great column of air,
 carried up towards the ash-filled sky, one of the first that day to glimpse
 the whole ball of the sun. She spoke heatedly of the warmth and excitement,
 but also of the danger, of the many ways in which the Fire was capable of
 reclaiming the lives it just spawned. That's what she was doing, her face
 lit from behind him by the setting sun, when the first Molly popped out
 of existence.
 For days the Fire and its remnants precipitated reddish spirits among whom
 Hex often heard tales of burning, rising, destruction. Thoughts
 of the Fire were in the air, exchanged by passerby spirits carried in
 currents for brief moments along similar trajectories. He found a Molly
 and reminded her of the day before, and saw that same spark in her
 eyes. They spent that day rolling like tumbleweeds through a nearby valley,
 talking in voices oscillating with their rotation.
 Recent days replaced the dying Fire with anxious winds. Though the sun at times
 still paints fields white-gold and turns trees' leaves to verdant haloes,
 the air feels heavy. Newborn spirits are a deep blue. Molly's latest iteration
 is an iridescent cornflower-cyan. Words that used to evoke in her a subtle smile,
 imagery that resonated with her, things that Hex has long since learned to
 sprinkle into their chats to see her light up --- all this seems now to have lost
 its potency. A knot forms in his stomach at the swelling thought that soon he
 will have nothing to say at all.
 It's the wind. It strengthens even now, augmented with dust, fragments
 of bark, torn leaves, fireflies. Dark clouds in the distance turn in circles
 on a pillow of rain-streak straw. Colored spirit-dots rush with helpless
 violence on the horizon. The storm draws nearer.
 They talk --- Hex still clumsily searching for words --- but it is becoming
 harder and harder to hear. The sky is polluted at first by pioneering clouds,
 then enveloped completely. The sun is shut out. The rain, not straw anymore
 but billowing sheets, beats against their faces. There is no way to see
 and speak except by facing away from this relentless onslaught. Water runs
 in miniature rivers down their faces. Their hands tightly grip their
 anchor-vine.
 Hex goes first. Slapped in the face with surprising force by a flying branch,
 he loses his grip and is carried immediately downwind. Molly grabs him
 with dexterity but halves thereby her own hold on the branch and mere
 seconds later is dislodged herself. The two cling to each other for a few
 moments before impacting rock and bouncing in different directions.
 Having joined the assembly of dislodged detritus Hex tumbles upwards.
 Ground alternates with sky in his vision, interspersed occasionally with
 glimpses of Molly's cyan. In a customary spirit gesture he reaches out his
 hands for something to grab but finds nothing but raindrops and hail. All
 the while he accelerates towards the clouds, his gravity bizarrely
 inverted; precipitation and debris increasingly obscure ground. At
 breakneck speed a yellow spirit beaten to foam whizzes past him to collide
 into a wind-blue byflyer in a pine explosion spewing polychrome droplets.
 The newly-acquainted pair exchange introductions that Hex can't make out
 over a deafening howling.
 With each crazed revolution around his axis he glances heavier objects in
 his vicinity. An entire birch, a survivor of the Fire unceremoniously
 uprooted by the Wind, scoops him with its willowy fingers and finally
 dilutes his momentum. The act of moving his head reacquires its familiar
 meaning. Hex dares to look around. Searchlight sunbeams pierce blackened
 clouds in rapid sweeps; lightning retaliates against the incursions in
 blinding, sprawling nets. Glimpses of brown flicker behind dense clouds
 and curtains of rain. Its orderly guidance of gravity and sunlight
 replaced by disagreeing gusts, a new forest orbiting an unseen center
 points in all directions at once. There is no sign of Molly.
 Above is indistinguishable now from below, and left from right. Directions
 other than _inward_ lose their meanings. Inward too flies Hex's
 birch-mount, and he with it. Lightning-lit glimpses of brown stretch
 finally into a continuous window.
 A vast beige clot levitates among the clouds, its colossal mass allowing
 it the luxury of unshakeable inertia. Dozens of armlike appendages
 protrude from its core, enormous in size compared to a single spirit's but
 spindly relative to the whole. A meteor of pine still engaged in
 conversation impacts the planetoid, sending a ripple through its body and
 forming a crown that is pulled as if by surface tension into a crater that
 rapidly narrows into nothing. A green band lingers on the giant's surface,
 then assimilates into the whole.
 The colossus endlessly speaks. Its low voice rumbles in competition with
 thunder. Hex is shaking either in feverish terror or in resonance
 with the creature's speech. "`nonlinear turbulence approximated with
 a third-order term,`" it espouses in a choral superposition of
 spirit-voices, "`a butterfly with no wing scales climbs yet towards the
 cosmos`". Then suddenly a flash of lucidity: "`selena, the wind, the
 wind's everywhere...`". In the pauses between its phrases and words,
 a rebellious mutter of overlapping conversations reasserts itself only to
 drown again in the giant's estimation of language. Its arm grasp the air
 in that same customary gesture but there is an uncanniness to their
 movement; Hex can't help but suspect that the intent behind them is
 entirely alien.
 With a sluggish wave "hello" towards no-one in particular, the giant sends
 Hex's tree into a new spiral just as the cycles of sunbeams all arrive at
 their individual troughs. The darkness drops again. The world spins
 dizzyingly around him while he clutches desperately for stability. When
 his vessel rights itself again, veering through some aerodynamic mystery
 into a semblance of stability, he listens once more to the colossus'
 endless tirade. At some point it must have given way to thunder. Specks of
 brown flicker in the distance. A spot of cornflower bobs nearby.
 Molly rides unsteadily on her own arborous steed. She has already spotted
 him, and waves excitedly, then reaches out her hand. It is now or never.
 Hex plants his feet on his birch, having finally found his sea legs in the
 atmospheric ocean. He feels his outwards-directed weight, tries to stand,
 wobbles, tries again. At last he musters whatever spring his sloshing body
 is capable of, and leaps.
 The spring turns out more than sufficient; he arrives with momentum to
 spare, grabbing Molly but dealing the final blow to her tentative hold on
 her tree and setting them both once again at the storm's mercy. She smiles
 and tries to speak, but he still can't hear. Hex wonders if she is
 remembering the Fire's column that lifted her that first day above the
 clouds. During his own birth, the flames had already cooled, but the hot
 air's purposeful ascent was not unlike the storm's lateral tug. But wait,
 he was born before Molly...
 Their eternity suspended in the directionless void gives way. Features of
 the landscape drift into view. Rain abates; clouds part. Lightning turns
 to distant flashes in the corners of their eyes and thunder's rumble
 fades. Still nearly weightless they remain swirling in the air until by
 some trick of their geometry familiar cliffs cut off the wind altogether
 and leave them to splash with their remaining speed into their ledge.
 They sit together in silence. His red-pink hand holds hers. For some time,
 they watch the landscape. Water drops from trees disturbed by wind as if
 from green straggler clouds. The setting sun colors the clearing horizon
 peach. The air is cool and crisp. Spirits form from pools of rainwater,
 flow along streams, and point luminescent eyes in wonder at the departing
 hurricane. An umber newborn's first words: "Magnificent! I just hope the
 butterflies are safe." Another responds, "I'm glad the turbulence is dying
 down".
 Molly and Hex have not moved from where they were deposited by the last of
 the storm's force, and this time he squints against sunlight that streams
 from behind her.
 "That was the strongest wind we've ever had! I'm glad I found you," Molly
 says. "There was so much chaos, but you seemed _at ease_ in the end.
 I guess it turned out pretty fun, but after all that floating, isn't it
 good to have some _weight_ again?" He can tell she's hinting at something,
 but he has no idea what that might be. Instead, he brings up the colossus
 in the clouds. What is it like to think the melange of thoughts of all
 spirits, each life enveloping the next like onion layers and tinting the
 final image? When it speaks its words, does it know what it means?
 Hex still can't find the right words. Molly saw the giant, but didn't
 think too much of it. He wants her to feel the mystery, the awe, the
 unease at its incomprehensible gestures. This is what he is doing, his
 face lit from behind her by the setting sun, when Hex pops again out of
 existence, leaving behind a gentle scent of soap.
--- a/content/writing/spirits/style.scss
+++ b/content/writing/spirits/style.scss
@@ -0,0 +1,25 @@
 $color-muted-plum: #3d2b3d;
 $color-ashy-orange: #4a3428;
 $color-storm: darken(#1e2a3d, 5%);
 html {
  background-color: $color-storm;
 }
 body {
  background-image: linear-gradient(
    180deg,
    $color-storm  0%,
    $color-muted-plum  5%,
    $color-ashy-orange 15%,
    $color-storm 100%,
  );
 }
 code {
  background: none;
  border: none;
  padding: 0;
  font-family: serif;
  font-variant-caps: small-caps;
 }
--- a/content/writing/thevoid/index.md
+++ b/content/writing/thevoid/index.md
@@ -1,7 +1,9 @@
 ---
 title: "Untitled Short Story"
 date: 2024-08-01T20:31:18-07:00
-type: thevoid
+description: "The Everpresent Void was first discovered at a children's birthday party."
 custom_css:
 - style.scss
 ---
 > I'm losing my edge to the art-school Brooklynites in little jackets and\
--- a/content/writing/thevoid/style.scss
+++ b/content/writing/thevoid/style.scss
@@ -1,50 +1,3 @@
@import "variables.scss";
 body {
  background-color: #1c1e26;
  font-family: $font-code;
 }
 h1, h2, h3, h4, h5, h6 {
  text-align: left;
  font-family: $font-code;
 }
 h1::after {
  content: "(writing)";
  font-size: 1rem;
  margin-left: 0.5em;
  position: relative;
  bottom: -0.5em;
  color: $primary-color;
 }
 nav .container {
  justify-content: flex-start;
  a {
    padding-left: 0;
    margin-right: 1em;
  }
 }
 .header-divider {
  visibility: hidden;
 }
 hr {
  height: auto;
  border: none;
  &::after {
    content: "* * *";
    color: $primary-color;
    font-size: 2rem;
    display: block;
    text-align: center;
  }
 }
 /* Code for the CSS glitch effect. Originally from: https://codepen.io/mattgrosswork/pen/VwprebG */
 .glitch {
--- a/convert.rb
+++ b/convert.rb
@@ -25,13 +25,16 @@ class KatexRenderer
  end
  def substitute(content)
    found_any = false
    rendered = content.gsub /\\\(((?:[^\\]|\\[^\)])*)\\\)/ do |match|
      found_any = true
      render(false, $~[1])
    end
    rendered = rendered.gsub /\$\$((?:[^\$]|$[^\$])*)\$\$/ do |match|
      found_any = true
      render(true, $~[1])
    end
-    return rendered
+    return rendered, found_any
  end
 end
@@ -58,8 +61,19 @@ renderer = KatexRenderer.new(katex)
 files.each do |file|
  puts "Rendering file: #{file}"
  document = Nokogiri::HTML.parse(File.open(file))
  found_any = false
  document.search('//*[not(ancestor-or-self::code or ancestor-or-self::script)]/text()').each do |t|
-    t.replace(renderer.substitute(t.content))
+    rendered, found_any_in_text = renderer.substitute(t.content)
    found_any ||= found_any_in_text
    t.replace(rendered)
  end
  found_any ||= document.at('meta[name="needs-latex"]')
  # If we didn't find any mathematical equations, no need to include KaTeX CSS.
  unless found_any
    document.css('link[href$="katex.css"], link[href$="katex.min.css"]').each(&:remove)
  end
  File.write(file, document.to_html(encoding: 'UTF-8'))
 end
--- a/data/submodules.json
+++ b/data/submodules.json
@@ -1,5 +1,5 @@
 {
-  "agda-spa": "https://dev.danilafe.com/DanilaFe/agda-spa/src/commit/828b652d3b9266e27ef7cf5a8a7fb82e3fd3133f",
+  "agda-spa": "https://dev.danilafe.com/DanilaFe/agda-spa/src/commit/913121488069a20cdfd40777a8777eb3744c415e",
  "aoc-2020": "https://dev.danilafe.com/Advent-of-Code/AdventOfCode-2020/src/commit/7a8503c3fe1aa7e624e4d8672aa9b56d24b4ba82",
  "blog-static-flake": "https://dev.danilafe.com/Nix-Configs/blog-static-flake/src/commit/67b47d9c298e7476c2ca211aac5c5fd961637b7b",
  "compiler": "https://dev.danilafe.com/DanilaFe/bloglang/src/commit/137455b0f4365ba3fd11c45ce49781cdbe829ec3",
--- a/layouts/_partials/spiderweb.html
+++ b/layouts/_partials/spiderweb.html
@@ -0,0 +1,4 @@
 <svg class="spiderweb" viewBox="0 0 197.21727 106.16592">
    {{ $spiderweb := resources.Get "svg/spiderweb.svg" | resources.Fingerprint }}
    <use href="{{ $spiderweb.Permalink }}#mainlayer"></use>
 </svg>
--- a/layouts/_shortcodes/donate_css.html
+++ b/layouts/_shortcodes/donate_css.html
@@ -0,0 +1,2 @@
 {{ $style := resources.Get "scss/donate.scss" | css.Sass | resources.Minify | resources.Fingerprint }}
 <link rel="stylesheet" href="{{ $style.Permalink }}" integrity="{{ $style.Data.Integrity }}">
--- a/layouts/_shortcodes/donation_method.html
+++ b/layouts/_shortcodes/donation_method.html
--- a/layouts/_shortcodes/donation_methods.html
+++ b/layouts/_shortcodes/donation_methods.html
--- a/layouts/_shortcodes/gmachine.html
+++ b/layouts/_shortcodes/gmachine.html
--- a/layouts/_shortcodes/gmachine_css.html
+++ b/layouts/_shortcodes/gmachine_css.html
@@ -0,0 +1,2 @@
 {{ $style := resources.Get "scss/gmachine.scss" | css.Sass | resources.Minify | resources.Fingerprint }}
 <link rel="stylesheet" href="{{ $style.Permalink }}" integrity="{{ $style.Data.Integrity }}">
--- a/layouts/_shortcodes/gmachine_inner.html
+++ b/layouts/_shortcodes/gmachine_inner.html
--- a/layouts/_shortcodes/halfpage.html
+++ b/layouts/_shortcodes/halfpage.html
@@ -0,0 +1,3 @@
 <div class="halfpage">
    {{ .Inner | markdownify }}
 </div>
--- a/layouts/_shortcodes/stack.html
+++ b/layouts/_shortcodes/stack.html
--- a/layouts/_shortcodes/stack_css.html
+++ b/layouts/_shortcodes/stack_css.html
@@ -0,0 +1,2 @@
 {{ $style := resources.Get "scss/stack.scss" | css.Sass | resources.Minify | resources.Fingerprint }}
 <link rel="stylesheet" href="{{ $style.Permalink }}" integrity="{{ $style.Data.Integrity }}">
--- a/layouts/_shortcodes/stack_element.html
+++ b/layouts/_shortcodes/stack_element.html
--- a/layouts/_shortcodes/stack_image.html
+++ b/layouts/_shortcodes/stack_image.html
--- a/layouts/_shortcodes/thevoid.html
+++ b/layouts/_shortcodes/thevoid.html
--- a/layouts/shortcodes/donate_css.html
+++ b/layouts/shortcodes/donate_css.html
@@ -1,2 +0,0 @@
 {{ $style := resources.Get "scss/donate.scss" | resources.ToCSS | resources.Minify }}
 <link rel="stylesheet" href="{{ $style.Permalink }}">
--- a/layouts/shortcodes/gmachine_css.html
+++ b/layouts/shortcodes/gmachine_css.html
@@ -1,2 +0,0 @@
 {{ $style := resources.Get "scss/gmachine.scss" | resources.ToCSS | resources.Minify }}
 <link rel="stylesheet" href="{{ $style.Permalink }}">
--- a/layouts/shortcodes/stack_css.html
+++ b/layouts/shortcodes/stack_css.html
@@ -1,2 +0,0 @@
 {{ $style := resources.Get "scss/stack.scss" | resources.ToCSS | resources.Minify }}
 <link rel="stylesheet" href="{{ $style.Permalink }}">
--- a/layouts/thevoid/baseof.html
+++ b/layouts/thevoid/baseof.html
@@ -1,20 +0,0 @@
 {{- /* Note: changing the baseof template because the title, tags, etc. of a regular post are still valid. */ -}}
 <!DOCTYPE html>
 <html lang="{{ .Site.Language.Lang }}">
    {{- partial "head.html" . -}}
    <body>
        {{ $voidcss := resources.Get "scss/thevoid.scss" | resources.ToCSS | resources.Minify }}
        <link rel="stylesheet" href="{{ $voidcss.Permalink }}">
        {{- partial "header.html" . -}}
        <div class="container"><hr class="header-divider"></div>
        <main class="container">
        {{- if .Draft -}}
        {{- partial "warning.html" (i18n "postDraft") -}}
        {{- end -}}
        {{- block "main" . }}{{- end }}
        </main>
        {{- block "after" . }}{{- end }}
    </body>
 </html>
--- a/themes/vanilla
+++ b/themes/vanilla
Author	SHA1	Message	Date
Danila Fedorin	4918558893	Tweak styles to make things work nicely with "page-looking things" Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-05-22 23:22:24 -07:00
Danila Fedorin	25f8e31fd3	Finish draft Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-05-22 22:48:12 -07:00
Danila Fedorin	f92b8bcab1	Add initial draft of Pynchon before repurposing Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-05-22 21:01:11 -07:00
Danila Fedorin	98e2e7da6c	Update theme with i18n stuff Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-05-19 17:55:47 -07:00
Danila Fedorin	f57e3d370b	Bump theme version Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-05-19 17:06:51 -07:00
Danila Fedorin	8795003ce7	Fix submodule links in SPA part 6 which got out of sync with the code Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-05-19 17:05:43 -07:00
Danila Fedorin	487681df16	Move bergamot.css and writing.css into theme Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-05-18 22:11:44 -07:00
Danila Fedorin	51964e1d9f	Add fingerprinting and integrity to custom CSS Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-05-18 21:46:58 -07:00
Danila Fedorin	3695dd561f	Update theme Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-05-18 21:36:15 -07:00
Danila Fedorin	38ae57792a	Move files into new Hugo format	2026-05-18 21:01:15 -07:00
Danila Fedorin	0b9612f138	Tweak config.toml and .gitignore per Codex's suggestions Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-05-18 21:00:39 -07:00
Danila Fedorin	ffca10f447	Update theme Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-05-12 22:05:23 -07:00
Danila Fedorin	e1efe0f406	Update theme and add thumbnails where available Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-05-06 18:57:32 -07:00
Danila Fedorin	99c9890c99	Remove explicit 'type' since it's set by convention Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-04-23 16:43:38 -07:00
Danila Fedorin	98c91dd643	Update theme Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-04-19 00:37:19 -07:00
Danila Fedorin	73f8c787c9	Merge all writing layouts into a single one Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-04-19 00:17:33 -07:00
Danila Fedorin	4a29854f7b	Add descriptions to the void and spiders.	2026-04-18 23:49:14 -07:00
Danila Fedorin	ac3804530c	Add custom style for spirits.	2026-04-18 23:48:09 -07:00
Danila Fedorin	8b9886cc8f	Finalize draft of spirits	2026-04-18 23:46:12 -07:00
Danila Fedorin	d672464de8	Add first complete draft Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-04-18 22:30:21 -07:00
Danila Fedorin	bcca964381	Add initial draft of spirits Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-04-18 11:09:47 -07:00
Danila Fedorin	bd10207cd2	Add missing images Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-04-05 16:23:45 -07:00
Danila Fedorin	00b810599a	Add descriptions to new articles Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-04-05 16:21:01 -07:00
Danila Fedorin	3403a28e35	Publish two new articles Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-04-05 16:19:06 -07:00
Danila Fedorin	53e638cb17	Use new flag to avoid deduplicating series Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-04-05 16:18:36 -07:00
Danila Fedorin	aabbc66bb2	Grammar pass Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-04-05 16:09:27 -07:00
Danila Fedorin	767545dda4	Update theme Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-04-05 16:02:27 -07:00
Danila Fedorin	f90760d66a	Add a link to the source code. Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-04-05 16:01:28 -07:00
Danila Fedorin	d696183690	Split into two files Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-04-05 16:00:31 -07:00
Danila Fedorin	21463ede20	Make some edits. Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-04-05 15:42:26 -07:00
Danila Fedorin	a278d1f572	Add initial (bundled) draft of flashcard writeup	2026-04-05 15:22:12 -07:00
Danila Fedorin	bdd2be48bd	Update theme Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-03-22 01:31:20 -05:00
Danila Fedorin	a350cd14f8	Publich 'On Spiders' Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-03-22 01:08:11 -05:00
Danila Fedorin	49ab3982f1	Extract writing CSS into a separate file from the void. Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-03-22 01:04:58 -05:00
Danila Fedorin	4d35ca04fe	Slightly tweak wording Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-01-19 10:23:02 -08:00
Danila Fedorin	5e117e3f48	Ignore warnings encoded as syntax highlighting Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-01-04 16:33:43 -08:00
Danila Fedorin	a6f3cd3f9a	Update theme. Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-01-03 18:08:51 -08:00
Danila Fedorin	ccc8d6f0eb	Re-enable hiding LaTeX Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-01-03 16:34:57 -08:00
Danila Fedorin	7a088d6739	Edit, finish, and publish post on PL Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-12-31 21:27:55 -08:00
Danila Fedorin	626baefd76	Do some aggressive trimming and editing. Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-12-30 00:06:17 -08:00
Danila Fedorin	4602d02720	[WIP] 2/3 draft Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-12-29 23:07:55 -08:00
Danila Fedorin	7fbd4ea9f8	Update theme with syntax highlighting fix Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-04-12 17:56:44 -07:00
Danila Fedorin	6fd1e1962b	Update theme Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-03-30 23:15:54 -07:00
Danila Fedorin	62c338e382	Add a post on Chapel's runtime types Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-03-02 22:56:10 -08:00
Danila Fedorin	40ea9ec637	Update theme for newer Hugo Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-03-02 19:00:05 -08:00
Danila Fedorin	787e194d41	Update theme with new Hugo support Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-03-02 13:42:42 -08:00
Danila Fedorin	71162e2db9	Update nokogiri more Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-03-02 13:36:08 -08:00
Danila Fedorin	43debc65e4	Update nokogiri Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-03-02 13:27:09 -08:00
Danila Fedorin	b07ea85b70	Update ruby scripts to use 'File.exist?' Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-03-02 11:32:55 -08:00
Danila Fedorin	06e8b8e022	Keep KaTeX css files Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-02-23 17:01:49 -08:00
Danila Fedorin	647f47a5f3	Remove KaTeX CSS includes if we don't need them. Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-02-23 14:43:49 -08:00
Danila Fedorin	36e4feb668	Update theme Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-02-23 14:14:15 -08:00
Danila Fedorin	11be991946	Print number of files processed	2025-02-23 13:25:18 -08:00
Danila Fedorin	a8c2b1d05a	Fix bug in subsetting script Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-02-23 13:16:33 -08:00
Danila Fedorin	fb46142e9d	Remove incorrect print Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-02-23 12:45:24 -08:00
Danila Fedorin	0b33d03b73	Pass the font folder as part of argv Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-02-23 12:35:45 -08:00
Danila Fedorin	804147caef	Read SVG path from the command line Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-02-23 12:34:44 -08:00
Danila Fedorin	d847d20666	Adjust Python script to also just accept HTML files as args Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-02-23 12:28:19 -08:00
Danila Fedorin	07408d01a9	Use ARGV like other ruby post-processing scripts Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-02-23 12:22:06 -08:00
Danila Fedorin	816a473913	Add a (ChatGPT-provided) script to perform subsetting Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-02-23 12:05:02 -08:00
Danila Fedorin	ce8f8fb872	Add a (ChatGPT-provided) script to subset feather icons Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-02-23 11:58:41 -08:00
Danila Fedorin	2f60004241	Update theme with instanced fonts Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-02-23 11:43:38 -08:00
Danila Fedorin	7130c6bd11	Fix cross-linking in whitespace-trimmed files Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-12-26 12:35:03 -08:00
Danila Fedorin	c5aacc060a	Update theme with font improvements Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-12-26 11:53:29 -08:00
Danila Fedorin	6048dc0b9c	Mark SPA series as completed Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-12-25 19:07:26 -08:00
Danila Fedorin	1f01c3caff	Publish the last two posts in the SPA series Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-12-25 19:05:28 -08:00
Danila Fedorin	bca44343eb	Update theme with required shortcodes Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-12-25 19:04:10 -08:00
Danila Fedorin	3b9c2edcdd	Write up the "verified" portion of the forward analysis Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-12-25 19:03:51 -08:00
Danila Fedorin	fa180ee24e	Fix thevoid theme on light mode devices Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-12-04 13:58:32 -08:00
Danila Fedorin	5846dd5d04	Fix typos Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-12-01 22:19:45 -08:00
Danila Fedorin	f6b347eb05	Fix slugs and add example of constant propagation Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-12-01 22:19:08 -08:00
Danila Fedorin	c1b27a13ae	Add a draft post on forward analysis Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-12-01 22:16:02 -08:00
Danila Fedorin	147658ee89	Update theme Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-11-28 20:41:21 -08:00
		`@@ -0,0 +1,2 @@`
							`{{ $style := resources.Get "scss/donate.scss" \| css.Sass \| resources.Minify \| resources.Fingerprint }}`
							`<link rel="stylesheet" href="{{ $style.Permalink }}" integrity="{{ $style.Data.Integrity }}">`
		`@@ -0,0 +1,2 @@`
							`{{ $style := resources.Get "scss/gmachine.scss" \| css.Sass \| resources.Minify \| resources.Fingerprint }}`
							`<link rel="stylesheet" href="{{ $style.Permalink }}" integrity="{{ $style.Data.Integrity }}">`
		`@@ -0,0 +1,2 @@`
							`{{ $style := resources.Get "scss/stack.scss" \| css.Sass \| resources.Minify \| resources.Fingerprint }}`
							`<link rel="stylesheet" href="{{ $style.Permalink }}" integrity="{{ $style.Data.Integrity }}">`
		`@@ -1,2 +0,0 @@`
			`{{ $style := resources.Get "scss/donate.scss" \| resources.ToCSS \| resources.Minify }}`
			`<link rel="stylesheet" href="{{ $style.Permalink }}">`