The project I’m working on requires me to formalise a proof in Coq, but the subject matter is mostly unrelated to mathematics—specifically, it has to do with software engineering principles. Using Coq, I want to confirm that a software system has the features of correctness, consistency, and safety.
I am rather proficient in the fundamental syntax and strategies of Coq, but I am having trouble converting my software needs and specifications into rigorous Coq statements & proofs. For instance, I have to demonstrate that a specific algorithm executes with data integrity intact. The algorithm comprises several component interactions and a variety of state changes.
Is there anyone who could offer advice or resources about the formalisation of these kinds of proofs in Coq? Are there any particular libraries or approaches that are more appropriate for this type of work?
Furthermore, it would be very beneficial if someone could offer examples of formalising non-mathematical themes in Coq or have experience with projects similar to this one.
Coq is very well suited for the domain of formal software analysis, for which there are deep links to foundation mathematics and type theory, to a point at which I personally wouldn’t even call it a non-mathematical domain in my own idiolect
I would suggest starting with this resource: Software Foundations, which serves as a great intro to Coq and using Coq to formally analyze software. I cannot recommend it enough!
Just note that what you are trying to do is a large undertaking, equivalent to a research project - so expect it to take much time to develop that which you require.
I know that there are a lot of developments using Coq for formal analysis of software, so there are undoubtedly libraries that implement some of the theories you will need. Unfortunately I have not surveyed them and like you I too would love some exposition on them.
One very exciting project is the CompCert C compiler, which to my knowledge developed a formal model of the semantics of C and then used that model to construct a compiler that has end-to-end proof that a given C program that the compiler compiles if successfully compiled obeys said semantics in its compilation - an amazing feat!
Hopefully some more examples get posted, but at any rate studying the Software Foundations book and doing the exercises should at least get the ball rolling!
,
