Comparing #Lean and #Rocq (formerly known as Coq)
I thought both were theorem provers, but it seems Rocq is more for building verifiable software, while Lean is for more classical math.
So Lean might be a better fit for the math explorations #LLMs and #AI #Agents are doing for solving problems.
This game (still) rocks.
I binge-completed the first four chapters some time in 2014, did the next four in 2016, and then sadly let the project of finishing "Software Foundations" sit idle for almost ten years. :(
Well, any time is infinitely better than never, so here I go with the significantly expanded 2025 edition!
https://softwarefoundations.cis.upenn.edu/
Image warning: Screenshot spoils the solution to one exercise.
The Rust programming language provides a safe alternative to C and C++ for system programming. In particular, it achieves memory safety with an ownership-based typing discipline, providing a notion of borrows as a restriction on aliasable pointers. The discipline of borrows is statically enforced by a component of the compiler called the borrow-checker. In their article published at the ICFP conference in 2024, Ho, Fromherz and Protzenko prove that LLBC, a borrow-centric model of Rust, can be equipped with a symbolic semantics that plays the role of a borrow-checker. They also prove that LLBC is a sound model with respect to an operational semantics over a standard memory model à la CompCert.<p>In this article, we initiate the formalization of this work in the Rocq proof assistant. In particular, we found a flaw in the proofs of some of their fundamental lemmas. We repair their methodology using techniques from rewriting theory. We finally present the current state of our formalization, and how we use a rewriting system to automate proofs.</p>
Fraser Tweedale
Guillaume Laforge
pesco
José A. Alonso