2 ms·
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 o
by rtpg 2y ago
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?
- LiamPowell 2y agoSPARK 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-that-it-can-sort https://blog.adacore.com/i-cant-believe-that-i-can-prove-tha...