> Homoiconicity anyone?

I'm just leaving this here for anyone interested, seems relevant: https://github.com/replikativ/ansatz

Ansatz is a verified programming library for Clojure built on the Calculus of Inductive Constructions (CIC) — the same type theory that powers Lean 4.