Zulip Chat Archive

Stream: general

Topic: Program verification


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jan 12 2019 at 14:51):

list.merge_sort is a verified sorting algorithm

view this post on Zulip Mario Carneiro (Jan 12 2019 at 14:51):

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

view this post on Zulip Mario Carneiro (Jan 12 2019 at 14:52):

they are pretty much all implemented

view this post on Zulip William Whistler (Jan 12 2019 at 14:52):

Thanks for the pointers!

view this post on Zulip Mario Carneiro (Jan 12 2019 at 14:53):

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

view this post on Zulip 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