this post was submitted on 07 Jul 2025
1 points (100.0% liked)

Formal Methods

190 readers
1 users here now

founded 2 years ago
MODERATORS
Ategon@programming.dev
synthetic_apriori@programming.dev
1
My first verified (imperative) program [Lean] (markushimmel.de)
submitted 2 days ago by armchair_progamer@programming.dev to c/formal_methods@programming.dev
0 comments fedilink hide all child comments
 

One of the many exciting new features in the upcoming Lean 4.22 release is a preview of the new verification infrastructure for proving properties of imperative programs. In this post, I’ll take a first look at this feature, show a simple example of what it can do, and compare it to similar tools.

no comments (yet)
sorted by: hot top controversial new old
there doesn't seem to be anything here