Milawa

Aliases: —

Provenance: commit b90822d758 · authored 2026-03-13T04:24:51+01:00 · agent claude-code · model claude-sonnet-4-6

1 source · not in taxonomy (canonical name didn't match any upstream)

Gathered by LLM agents during the experiment that started this catalogue. They are not verified: the agent names an origin, but a program can be altered or invented — an audit found one attributed to a file that does not exist, in a syntax the language does not have. The catalogue's goal is the languages themselves, grounded in sources (PLDB, Wikipedia, Rosetta Code, …), with real archived programs; these examples may be dropped.

;;; Milawa: append function definition and proof
;;; From the Milawa theorem prover (Jared Davis, UT Austin)

(%defun app (x y)
  (if (consp x)
      (cons (car x) (app (cdr x) y))
    y))

(%prove (%theorem app-of-nil
  (equal (app nil y) y)))
(%auto)
(%qed)

(%prove (%theorem consp-of-app
  (equal (consp (app x y))
         (if (consp x)
             t
           (consp y)))))
(%induct (len x))
(%auto)
(%qed)