I intend to teach students how to discharge SPARK VCs with Coq.
The motivation is that sometimes, you need interactive theorem proving to prove the properties you’d like to prove.
I started with this from the SPARK User’s Guide:
I then tried discharging all VCs with Coq in the SPARK Lab of this course:
This was reasonably easy for swap.adb and search_arr_zero.adb , but got real ugly real fast for the other ones. While I am not very experienced with Coq (I did Vol. 1-2 of Software Foundations, but that was a long time ago), it seems to me that proving VCs in Coq does not scale; they get really hard to discharge in Coq.
Notably, the VCs in Coq make no sense to me. I know they are something that SPARK needs to finish a proof (and therefore, the VC does not need to make sense, provided we trust SPARK). But still; if the VC made more sense, then it would be easier to come up with a proof idea, to then implement in Coq.
I then looked around the Internet to see if anyone actually has used Coq to discharge VCs, and I did not find anyone who has done so. Even the VerifyThis! SPARK solution does not do so (thus leaving the challenges that need interactive proofs, unsolved).
Finally, I needed to install an older version of Coq to do this exercise (since this feature only worked for that version of Coq). Setting that up was (very doable, albeit) a bit painful.
Is this something that people just don’t do? Do people use other features in SPARK (e.g. ghost code), or just turn to other tools, when automated theorem proving fails? Is this ability to discharge SPARK VCs with Coq more of a “proof of concept” / “fun demo” / “in case anyone needs it”?
If this feature is really meant for proving properties of software in industry, then I would very much value any comments, hints, pointers, or reading, on how to do this. For instance, are there certain Coq libraries / tactics that makes discharging the VCs in Coq easier? Is there some rule-of-thumb / paradigm I should follow to make whatever SPARK cannot discharge automatically as small and simple as possible?