Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Lf-lean: The frontier of verified software engineering

theorem.dev

Post reply on HN
Print view View original

1–10 of 12 posts

Re: Lf-lean: The frontier of verified software engineering

#2

Post by ngruhn »

Is this impressive? They just ported a bunch of theorems/proofs already written in Rocq into Lean. Also Logical Foundations is just a Rocq tutorial with the basics. An absolutely amazing tutorial and probably the best resource out there. But I'm not surprised AI can do that.

Re: Lf-lean: The frontier of verified software engineering

#3

Post by benlivengood »

ngruhn wrote: post #2

Is this impressive? They just ported a bunch of theorems/proofs already written in Rocq into Lean. Also Logical Foundations is just a Rocq tutorial with the basics. An absolutely amazing tutorial and probably the best resource out there. But I'm not surprised AI can do that.

Impressive if for no other reason than there are various disparate formally verified projects (seL4, compcert, certikos) that could potentially be unified under a single proof system. Additionally it may be possible to quickly extend existing proofs (e.g. seL4's proofs) to other architectures.

Re: Lf-lean: The frontier of verified software engineering

#4

Post by ngruhn »

benlivengood wrote: post #3
ngruhn wrote: post #2

Is this impressive? They just ported a bunch of theorems/proofs already written in Rocq into Lean. Also Logical Foundations is just a Rocq tutorial with the basics. An absolutely amazing tutorial and probably the best resource out there. But I'm not surprised AI can do that.

Impressive if for no other reason than there are various disparate formally verified projects (seL4, compcert, certikos) that could potentially be unified under a single proof system. Additionally it may be possible to quickly extend existing proofs (e.g. seL4's proofs) to other architectures.

Not saying this is useless. But that article reads like they made some kind of breakthrough in automatic software verification. But is sounds like they rather ported a tutorial test suite from Go to Rust with AI and the tests are still passing.

Re: Lf-lean: The frontier of verified software engineering

#6

Post by corysama »

ngruhn wrote: post #2

Is this impressive? They just ported a bunch of theorems/proofs already written in Rocq into Lean. Also Logical Foundations is just a Rocq tutorial with the basics. An absolutely amazing tutorial and probably the best resource out there. But I'm not surprised AI can do that.

I believe what they are bragging about is not the translated proofs, but the process of doing the translation.

> produced by frontier AI with ~2 person-days of human effort versus an estimated ~2.75 person-years manually (a 350x speed-up). We achieve this through task-level specification generators...

Re: Lf-lean: The frontier of verified software engineering

#8

Post by nextos »

It's interesting Lean is taking off in software engineering. Prior to the advent of LLMs & agents, Lean had almost zero use in software and was mostly focused on mathematics, with Isabelle and Rocq leading the way here. In fact, I asked Kevin Buzzard and others in the Lean community, and they simply shrugged.

The exception was [1], a Lean-based text heavily inspired by Concrete Semantics [2], a cornerstone of Isabelle literature. The latter is, in essence, Winskel's classic semantics book [3], a standard textbook in programming language theory, with all proofs mechanically checked.

More broadly, I'm wondering whether dependent types are the right abstraction or too powerful and heavy for humans to review and make sure specifications are aligned with intent. I've been working on automation for this for more than a year, and I've found refinement types sufficient and much easier to review.

[1] https://github.com/lean-forward/logical_verification_2025

[2] http://concrete-semantics.org

[3] https://direct.mit.edu/books/monograph/4338/The-Formal-Seman...

Post reply on HN