Last week I put work off for Future Me, and without realizing I have become Future Me. How does she always get me???

Making a OCaml parser combinator library for fun! I’m going with an applicative interface instead of the standard monadic interface, which should allow me to get much better performance and error messages. It does restrict you to context-free grammars though, but that’s not much of a restriction

I wonder if it’s possible to create a language-agnostic structured editor 🤔

I’ve had people ask me “what is type theory” and the best answer I’ve been able to come up with is “the study of notions of well-formed syntax, and what properties that well-formedness implies”. For instance, for most languages well-formedness wrt the type system implies some sort of safety…

I used to use Agda a lot, but tbh I'm much more satisfied with Coq for large-scale developments, the primary reason being Agda's proof automation is a lot less mature. That's something that can just be improved with time though, I wonder if anyone's made a tactic framework for Agda! #proofassistants

Something people often get confused about is the relationship between type theory and set theory. You can think about it with this (somewhat ridiculous) metaphor: Type theory is like a poem, and set theory is like an *interpretation* of the poem. Let's dive into that a little more... 🧵

OCaml's `Dynlink` module is so cool! I'm realizing that this is probably how Coq implements plugins? It's how I'm doing it in the proof assistant I'm implementing anyway. Hoping to have something usable soon... flip-flopped so many times on the design haha

Been using OCaml a lot recently and loving it. Type parameters being backwards is a little weird, but that’s fine. Overall it’s a clean, consistent, expressive language that sets up nice guardrails without forcing you to stay inside them. I get why people say ML is a language design sweet-spot!

Fun fact: You are topologically equivalent to a 7-holed donut, and thanks to homotopy type theory that means you are also equivalent to a certain higher-inductive type.

Thank you for attending my TED talk.

The biggest issue I’ve noticed that every person who learns Prolog brings up is the lack of informative runtime errors. Instead of a nice crash message or whatever, you just get `false`.

I like logic programming! But this is a big issue it has. It comes down to something more fundamental though…

Thinking about metalanguages for proof assistants… in theorem proving systems we almost always have some sort of proof automation, and if we want to create our *own* proof automation then we need some sort of metaprogramming. In Agda this is reflection, in Coq this is Ltac, etc… 🧵