I’m curious whether people can use Lean primarily as a software specification language, without necessarily intending to prove everything.
Can we use it to specify module meanings and laws, to make the design precise and checkable, and would allow us to implement property based tests for those laws in our implementation. Lean becomes a tool for more precise thinking about the design.
Yes, absolutely. There's been a lot of work along these lines in other interactive theorem provers like Isabelle/HOL and Rocq. The general term to search is "Hoare logic," and I'm also a fan of the Concrete Semantics textbook. Lean is a very flexible language, but the main downside with Lean is that libraries for reasoning about program logic are comparatively less developed than Mathlib is for math.
woggy · · focus · HN ↗
Can we use it to specify module meanings and laws, to make the design precise and checkable, and would allow us to implement property based tests for those laws in our implementation. Lean becomes a tool for more precise thinking about the design.
keeganryan · · focus · HN ↗
rramadass · · focus · HN ↗