Charleston Lean Proof Assistant Meetup

Lean is a functional programming language with a highly expressive type system. It can be used to produce performant programs that are guaranteed to meet their specifications, which proves that a large class of bugs cannot exist in your program. It can also be used to interactively prove theorems in mathematics. This meetup is for enthusiasts to join together to learn, code, and share their experiences with Lean.

For our third meeting, we will talk about using Lean to provide guarantees about data structures which are useful real world software. In particular, we will look at arrays and vectors. The arrays require a proof obligation for access at a given index. The vectors have their size included in its type. Additionally, we will show how to use the Lean tooling to configure, build, and run a small program.