upvote
I have been writing my own programming language _completely in lean_, from the parser down to the compiler.

My current workflow is i have a coordinating agent, and then a bunch of long running sessions that are specialized (CS theory, Kernel, Surface, Lowering/Backend, Corpus, Docs, etc). I only talk to the coordinator, they only accept tasks from the coordinator, but they can ask each other questions. None of them do their own coding, they assign coding tasks to agents/workflows. The main purpose of that is to stop it from blowing out context windows. Each has a million tokens of long term context and their own memory/claude.md etc, and they don't waste it by writing code directly. All work is assigned via github issues and answered with PRs. The coordinator mostly just keeps big picture goals in mind and manages PRs, etc..

I've currently got a fully formally verified borrow calculus and effect algebra, with a formally verified guarantee of memory safety and that all programs either continue (don't get wedged, no deadlocks), or they terminate with the heap empty. The only thing _not_ formally verified is the lowering to LLVM.

The language is mature to the point that I have real programs in it...

reply