[raphinou]

Can this be useful for someone with no prior knowledge of lean? I'd like to verify a software I'm working on, but I have no experience in formal verification. Can I get useful result with the spec, the code and some (limited) learning time on my side?

[reinitctxoffset]

I've gone from zero knowledge of lean4 to the point where I'm doing most of my coding with it in ~6 months, and this was dramatically helped by how facile the AI assist is: it's remarkable how consistently fluent models are in lean4. I've found this to be true of the near frontier and smaller local models alike, LLMs just seem to get lean4.

I still have a ways to go before calling myself a lean4 expert, but I don't need assist to get useful programs anymore.

The ability to start with very little knowledge and still be able to trust parts you don't fully understand is a real unlock on learning progress: it's both practical and motivating to get useful programs you can rely on with incomplete knowledge, it sort of drags you in. You're bounded by the subset of the language that describes your axiom and proposition surface, not the subset that describes the intermediate steps. Over time as your ambition goes up, you need to understand more to do more things, but you can operate safely at level N+1 in a sense.

It's also just a delightful programming language irrespective of its theorem proving role, and it's remarkably fast. I've got it bolted to io_uring and in many cases it blows the ass off of C++ with libuv or Rust with Tokio. Now and again you'll see some huge tail at the p99.99 latency or something and you go make a number fixed width or something, but you have to tune C++ and Rust too.

[andrewcl]

Any chance you can share any of your process? Super interesting to hear you use lean as a meta language, I'd be curious to see how you've harnessed this (as I'd like to do the same)!

[reinitctxoffset]

I hope to open source some of this soon but it's still married to quirky internal build tools and other jank. I'll make a note to come back to this comment when there's code up.

In terms of process I don't know that I really have any unique edge or anything, I'm still very intermediate as a lean4 programmer. I was a strong Haskeller before so I had a little bit of a map. The key thing about lean4 coming from e.g Haskell is that it has a much cleaner type tower, there's no type/kind/PolyKind jank, it's just Type 0, Type 1, as high as you care to go (which usually isn't very high), so a fair bit is unlearning some of that.

A mistake I made was to try to learn lean4 in emacs, which I'm working on making more reasonable, but today lean4 is a vscode only experience IMHO, this is partially because the default Mathlib4 style is really unapproachable without the tooling (not being a professional mathematician I'll stop short of calling the style bad, maybe it's intuitive to mathematicians, but it's very ill suited for programming in the large as a hacker would approach it). Proofs of theorems are this tactic match space with a lot of implicit projection up into a big possibility space at every step, and then the next explicit tactic is grabbing things from that space often very implicitly. It's my least favorite part of the semantics (or maybe one I feel is over-used, there are ways to make it more explicit, the canonical example is probably `simp_only` which grounds in specific lemmas).

The effectful part of the language should be a pretty short hop from anything else with do-notation, it reads very naturally and the conditional/looping/match stuff sorta looks like Rust if you squint a little. One place the AI assist really shines is to go rename all the variables something reasonable, a lot of otherwise great code looks like it hybridized with a bizarre Hungarian-notation splinter faction, the keywords are fine.

There's some stuff that probably makes a lot of sense in a meta mathematical view of things that makes zero sense from a TCB standpoint. To mathematicians there is a distinction between the map coloring proof and Wiles' FLT proof. This is real and it makes sense in mathematics. But in high-assurance software having an issue with `native_decide` as opposed to `bv_decide` is a weird religion: TCB certifying them is identically compromised by a compromised compiler.

So I think it's mostly just a very small community trying to write code as the primary activity and layering on formal methods as a correctness strategy as opposed to a much bigger community doing real maths where the programming language is more of an amenity than the main show.

I suppose my approach is to be willing to go a different way in a different use case.

[numeri]

Are you writing general use programs in it, then? Have any good examples?

[reinitctxoffset]

It's early days of using it as a general purpose programming language, my initial use case was using it as a metaprogramming framework that lowered into target languages with some rigor on correspondence of the lowered artifact and the proof-amenable surface. By lines of code the biggest use case historically was describing state machines and codecs/protocols for high-assurance IO primitives: define QUIC or ZMTP once and get idealized performance C++ and Rust and Haskell (Zig coming soon) protocol suite native to io_uring.

Another big use case is GPU kernel compilation. I've encoded the polyhedral algebra used by CuTe and all of the stated theorems from nvfuser in lean4. From this you can recover scheduling and tiling properties that must be met to get equal or better performance to CASK (likely optimal) for many operations, and then lower that to PTX. Surprisingly often the candidate set for the fastest possible kernel turns out to be finite and enumerable, so fast inference.

Somewhat recently I started benchmarking stuff just directly in lean4 with a very small TCB shim to e.g. io_uring. I've done like the basic systems programming ABCs (I've got a reverse proxy that's lean4 and ~100 lines of C and shatters nginx, faster at every point on the histogram, memory use flat as a strap). Lithe runs on it so I can do web serving as fast as anything in the hyper ecosystem.

Now that I've got my feet with it I'm digging in on a serious project which is a hypervisor that addresses the deficiencies in firecracker. This is a place where some proven properties can really get you a lot of performance (something like firecracker has to be very defensive regarding e.g. virtqueue semantics in the presence of a malicious guest). Firecracker is an exceptional piece of code and it's carried me far but at agent scale it's time to go another turn of the crank on virtualization performance.

[barrenko]

God damn.

[barrenko]

+1, what is it that you are doing.

[rzmmm]

You need to understand the bits you are trying to prove, but not the full proof. It's more like reading haskell types than math, even though the vocabulary is heavily inspired by math.

[camkego]

Read this section of the article “ Bug Discovery: Finding Hidden Flaws”, they appear to have used the model on open source Rust to find issues starting with just the Rust code. You might be also able to have conversations that help you write the Lean to verify your application, but I’m not certain about this.

[rubendev]

I think at minimum you would need to understand which theorems you want to prove about your code, and how to express those in Lean. Otherwise you won’t be able to verify the output. It may have proven some statement that is machine checked to be correct, but it’s pointless if you don’t understand what that statement means and if it covers what you want to verify about your code.