Welcome

2026-07-26

You found the tend blog. tend is a personal task manager being written in Lean 4, and this blog is the lab notebook: every post documents a real step in building it, in order, starting from nothing. If you can read Haskell, you can read this — we will only stop to explain the parts where Lean actually differs, and skip the parts you already know.

Obligatory proof of life:

-- Looks like Haskell, runs strict.
def main : IO Unit :=
  IO.println s!"hello, {2 ^ 5} worlds"

#eval main  -- try this in your editor; no GHCi session required

Posts are numbered, 001 onward, and each one maps to actual commits in the repo, so you can check out the code and follow along. No frameworks, no magic: just lake, an editor, and a growing pile of .lean files. Start at the top of the index and read in order.

The itch: task data as code, code as Lean

Every task app imposes its ontology – projects hold lists hold tasks, take it or leave it – and keeps your data in a database you can’t grep. tend takes the opposite bet: tasks live in .lean source files you edit, grep, and version like everything else you own, and the organizing structures (lists, projects, views) are functions you write, not features you settle for. The data model is one thing: a graph.

The other half of the itch is selfish: learning Lean properly means building something used daily, and a task manager is the ideal victim – known domain, daily feedback loop, worst-case bug is a missed chore. See the README for the full manifesto. If you want a full-course textbook to go with this lab notebook, Functional Programming in Lean is the one written for people like us.

Boring setup: nix, lake, just watch

Three files and we never speak of it again. A nix flake pins the toolchain (lean4 – which ships lake, Lean’s cabal – plus just and watchexec); a lakefile.toml of five lines declares one library and one executable; a justfile refuses to run outside the devshell and offers two verbs:

just run     # lake exe tend
just watch   # ghcid -T :main, Lean edition: rebuild & rerun on save

And your ghcid reflex has an upgrade waiting: put #eval main (or #eval any expression) in a file, and the language server evaluates it in the editor as you type – per-declaration, incremental, no save required. The terminal watch loop is for output; the editor is where the feedback lives.