Hacker News Reader

Comment by justboy1987 | Hacker News Reader

justboy1987·

[flagged]

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.

In addition to Cedar:

[1] SymCrypt (MSR). Verified cryptographic primitives. It's in the latter style, using the Aeneas model of Rust.

[2] KLR (AWS). ML compiler. Not verified, but it's in the former style where they use pure Lean functions and interface with C code across the FFI.

[3] SampCert (AWS). Verified random sampling algorithms for differential privacy. Uses pure Lean functions and is called into via the reverse FFI.

Full disclosure I worked on 2 and 3 haha. There's also some stuff being used by cryptocurrency people but I don't follow that very closely.

[1] https://www.microsoft.com/en-us/research/blog/rewriting-symc... [2] https://github.com/leanprover/KLR [3] https://github.com/leanprover/SampCert

Reply on news.ycombinator.com