Something has been forming in the last few months. A small but distinct category of programming languages is appearing, aimed not at the humans writing the code but at the agents writing most of it. They agree on the diagnosis: agents are good at producing code and are increasingly bad to trust with it as the surface area grows, and the language itself should help. They diverge on the cure. This is one of them. Vow is a small, statically typed systems language whose programs carry machine-checked vows: preconditions, postconditions, and invariants verified by ESBMC bounded model checking before the code ships. The compiler is written in Vow. The verification side, which is the whole point, still needs hardening, and that's the work of the coming months. I'm announcing it now because the moment is here and there is more value in planting a flag than in waiting until everything is polished. The repo is at github.com/vow-lang/vow. Here's a SAT solver written in Vow, compiled by Vow,…
No comments yet. Log in to reply on the Fediverse. Comments will appear here.