diff --git a/.gitignore b/.gitignore
index c1162d6..dcd5aba 100644
--- a/.gitignore
+++ b/.gitignore
@@ -7,4 +7,3 @@ configure
 *.gz
 *.xz
 *.zst
-coq
diff --git a/coq/.gitignore b/coq/.gitignore
new file mode 100644
index 0000000..d05b2a0
--- /dev/null
+++ b/coq/.gitignore
@@ -0,0 +1,5 @@
+.Makefile.coq.d
+Makefile.cq
+Makefile.coq.conf
+doc
+Makefile.coq
diff --git a/coq/Makefile b/coq/Makefile
new file mode 100644
index 0000000..5b5d090
--- /dev/null
+++ b/coq/Makefile
@@ -0,0 +1,24 @@
+# Taken from <https://github.com/coq-community/manifesto/wiki/Recommended-Project-Structure>
+all: Makefile.coq
+	@+$(MAKE) -f Makefile.coq all
+
+clean: Makefile.coq
+	@+$(MAKE) -f Makefile.coq cleanall
+	@rm -f Makefile.coq Makefile.coq.conf
+	@rm -rf doc
+
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
+
+force _CoqProject Makefile: ;
+
+DOCDIR := doc
+
+doc:
+	@test -d doc || mkdir doc
+	coqdoc --html --utf8 -d doc/ theories/wf.v
+
+%: Makefile.coq force
+	@+$(MAKE) -f Makefile.coq $@
+
+.PHONY: all clean force doc
diff --git a/coq/README.org b/coq/README.org
new file mode 100644
index 0000000..2f106ea
--- /dev/null
+++ b/coq/README.org
@@ -0,0 +1,12 @@
+#+TITLE: README
+#+DESCRIPTION: A Coq development of Damerau-Levenshtein edit distance
+#+DATE: <2024-09-03 Tue 13:52>
+#+AUTODATE: t
+#+AUTHOR: Michael Herstine
+#+EMAIL: sp1ff@pobox.com
+#+OPTIONS: toc:nil org-md-headline-style:setext *:t ^:nil ^:{}
+
+* Introduction
+
+This directory contains a [[https://coq.inria.fr/][Coq]] development of Damerau-Levenshtein edit distance. It's my first Coq development, so please don't judge it too harshly.
+
diff --git a/coq/_CoqProject b/coq/_CoqProject
new file mode 100644
index 0000000..e75431d
--- /dev/null
+++ b/coq/_CoqProject
@@ -0,0 +1,3 @@
+-Q theories DamerauLevenshtein
+
+theories/wf.v
diff --git a/coq/theories/.gitignore b/coq/theories/.gitignore
new file mode 100644
index 0000000..2001099
--- /dev/null
+++ b/coq/theories/.gitignore
@@ -0,0 +1,8 @@
+.lia.cache
+*.aux
+*.glob
+*.vo
+*.vok
+*.vos
+.old-files
+
diff --git a/coq/theories/wf.v b/coq/theories/wf.v
new file mode 100644
index 0000000..1d6a6d7
--- /dev/null
+++ b/coq/theories/wf.v
@@ -0,0 +1,53 @@
+(* Copyright (C) 2024 Michael Herstine *)
+
+Require Import Coq.Arith.PeanoNat.
+Require Import Lia.
+
+(** * Introduction *)
+
+(** This is my attempted formalization of "The String-to-String
+    Correction Problem" by Wagner & Fischer:
+
+    Wagner, Robert A., and Michael J. Fischer. 1974. "The
+    String-to-String Correction Problem." Journal of the Acm 21 (1):
+    168-73. https://doi.org/10.1145/321796.321811.
+
+    I started with Wagner & Lowrance, but found it to be difficult to
+    formalize. Perhaps related is the fact that Ukkonen, the next step
+    in the evolution of these algorithms, bases his work on Wagner &
+    Fischer.
+
+    This is my first non-trivial Coq development, so it's going to be
+    quite chatty as I figure things out. *)
+
+(** * Preliminaries *)
+
+(** Throughout, let [a] & [b] be strings. While Wagner & Fischer use
+    capital letters for their strings, that conflicts with Coq naming
+    conventions, so I'm going to switch to lower-case. I first thought
+    to use the stdlib [string] to represent them, but found that List
+    is much more featureful, so instead I'll just use a List of Ascii.
+    *)
+
+Require Import Ascii.
+
+Open Scope char_scope.
+Definition c := "c".
+Definition a := "097".
+Print a. (** :=> "a" : ascii-- 'a' is ASCII code 97 *)
+
+Close Scope char_scope.
+Reset c.
+
+(** I've played a bit with [Vector.t], but like others found it a bit
+    tedious to work with. John Wiegley has some interesting
+    alternatives here
+    <https://stackoverflow.com/questions/42302300/which-vector-library-to-use-in-coq>,
+    but for now let's just use lists: *)
+
+Require Import List.
+Import ListNotations.
+
+Definition string := list ascii.
+
+Compute ["H";"e";"l";"l";"o"].