## Stream: general

### Topic: Program verification

#### William Whistler (Jan 12 2019 at 14:49):

The stub for the program verification chapter in "Programming in Lean" says "Give some natural examples, for example, proving properties of functions of lists, sorting routines, properties of the extended gcd. Discuss two styles: separating functions and properties, and combining them, using subtypes."

Are any of these examples implemented, even though the chapter is incomplete? Alternatively, are there any other particularly nice examples of such proofs that someone could point me at?

#### Mario Carneiro (Jan 12 2019 at 14:51):

list.merge_sort is a verified sorting algorithm

#### Mario Carneiro (Jan 12 2019 at 14:51):

list.reverse_reverse is a classic example of proving a property of a program

#### Mario Carneiro (Jan 12 2019 at 14:52):

they are pretty much all implemented

#### William Whistler (Jan 12 2019 at 14:52):

Thanks for the pointers!

#### Mario Carneiro (Jan 12 2019 at 14:53):

Most of the mathlib examples use the "separate function and properties" style

#### Mario Carneiro (Jan 12 2019 at 14:54):

Minchao Wu presented a pretty good example of the "dependent types" proof approach at lean together this week

Last updated: May 14 2021 at 06:16 UTC