formal verification

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.

The Rust Effects Debate and Concrete's Case for a Smaller Language The Rust Effects Debate and Concrete’s Case for a Smaller Language
9 min read Keywords:  Programming Languages, Formal Verification, rust, Type Systems, lean

Wuyts is right about effects and ownership. The Hacker News skeptics are right about complexity. Concrete accepts both and says no to refinement types.

The Concrete Programming Language: Systems Programming for Formal Reasoning The Concrete Programming Language: Systems Programming for Formal Reasoning
38 min read Keywords:  Programming Languages, Formal Verification, Type Systems, lean

Concrete is a systems language proposal built for machine reasoning, aiming to combine low-level performance with formal verification, safety, and expressive design.