|
|
|
|
|
|
by touisteur
1 day ago
|
|
|
Yes it gets hard really fast. We had a fun (if tongue-in-cheek) exploration of this (proving a sort implementation) with Yannick Moy of SPARK fame some time ago https://www.adacore.com/blog/i-cant-believe-that-i-can-prove... I only regret not writing the obvious-but-buggy code that "forgot" or added some values and still passed proof... |
|
|