4 ms·
It's formal verification that works with proofs. Like coq, agda, lean, with which e.g. they proven the Navier-Stokes. This is a new such language. Assertions a
by gf000 8d ago
It's formal verification that works with proofs. Like coq, agda, lean, with which e.g. they proven the Navier-Stokes. This is a new such language.
Assertions and constraint programming is often runtime only. These languages use dependent types and verify the proves at compile time.
- YeGoblynQueenne 8d agoIt's not exactly like a proof assistant because it has a built-in generate-and-test loop: an LLM generates code until the code passes verification. Basically that's all of AI nowadays: generate-and-test loops. It's like the 1950's all over again.