Program verification

Stream: general

[William Whistler]

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]

list.merge_sort is a verified sorting algorithm

[Mario Carneiro]

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

[Mario Carneiro]

they are pretty much all implemented

[William Whistler]

Thanks for the pointers!

[Mario Carneiro]

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

[Mario Carneiro]

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