Comment by wazHFsRy
4 months ago
Does that mean your production code is lean? Or do you translate some other language code to lean to verify it?
4 months ago
Does that mean your production code is lean? Or do you translate some other language code to lean to verify it?
Also a very good question btw, people do both. For some projects Lean is expressive and performant enough to use on its own (or call into using the reverse FFI), other projects use a model of a real programming language like Rust. The disadvantage of the latter is that the Lean model of Rust has to be trusted.
Do you know if there are some resources or examples of this? Especially actual production stuff, not just side projects or proof of concepts?
Cedar (https://lean-lang.org/use-cases/cedar/) at AWS use an executable Lean model of a system as an oracle for differential testing of a Rust implementation. If you can't run Lean in production, then their approach is compelling.
The idea is that you start with a Lean specification, create a fully verified implementation with respect to the spec, and then hook it and the production implementation up to a fuzzer or source or random inputs. Then you can explore a lot of the state space fully automatically.
2 replies →