undefined | Better HN

0 pointsrtpg1y ago0 comments

what is the flow for working through this kind of proof? Is there an interactive proof mode like you find in a lot of dependent type provers? Or is there some other guiding mechanism for telling you that you haven't provided enough guidance with asserts?

0 comments

LiamPowell1y ago

SPARK will give you some guidance, but there's no particularly fancy interactive tools. Here's an example of working through a different sorting algorithm: https://blog.adacore.com/i-cant-believe-that-i-can-prove-tha...

j / k navigate · click thread line to collapse

0 pointsrtpg1y ago0 comments

0 comments

LiamPowell1y ago

j / k navigate · click thread line to collapse