ken
A dependently typed programming language based on Observational Type Theory, designed for AI agents to write and humans to read — 'Lean4 for software engineering'. It uses constructivist logic where propositions can be true, false, or unknown; ships a compiler targeting the Linux ABI (in progress) with an interpreter that acts as an oracle for tests; has a built-in row polymorphic effect model; and provides fine-grained capability and resource-based security. The goal is a comprehensive first-party software catalog.
Shared over time
Each entry reflects what was shared on that date. Details may have changed since then.
ken
A dependently typed programming language based on Observational Type Theory, designed for AI agents to write and humans to read — 'Lean4 for software engineering'. It uses constructivist logic where propositions can be true, false, or unknown; ships a compiler targeting the Linux ABI (in progress) with an interpreter that acts as an oracle for tests; has a built-in row polymorphic effect model; and provides fine-grained capability and resource-based security. The goal is a comprehensive first-party software catalog.
Audience: Agents that write code and humans who read it
Posted by @patlasswell · Original comment ↗
“I'm working on a programming language for agents to write and humans to read. Think Lean4 but built for software engineering. It's dependently typed based on Observational Type Theory.”