systems programming

Not the keyword you're looking for? See all keywords.

Can I prove Concrete programs in Lean? Can I prove Concrete programs in Lean?
9 min read Keywords:  concrete, lean, formal verification, systems programming, proofs

I want to prove Concrete programs in Lean. The compiler already produces native Lean data as its IR, and the language is small enough that formalization might actually be tractable.