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. A few key differences from Lean4:
1. Constructivist rather than propositional logic, so propositions can be true or false or unknown.
2. Compiler which targets the Linux ABI (in progress). An interpreter exists and acts as an oracle for tests.
3. Built-in row polymorphic effect model.
4. Fine-grained capability and resource-based security.
I aspire for it to have a comprehensive first-party software catalog.