Formal verification
About formal specification of software in Coq/Rocq.
There is a lot to proof - a truth that holds in all circumstances.
I am using Coq (soon to be renamed to Rocq) for the formalisation of the software eLyKseeR. This means that the end result, the software, will behave as specified by the formalisation. And, this can be proved.
in short..
A short overview what Coq is: https://coq.inria.fr/a-short-introduction-to-coq
The most important property is that a program or function will eventually finish its computation once started. All functions in Coq need to be written in a style that this is proven. Otherwise, the theorem prover will complain.
More properties can be written as lemmas or theorems in Coq and they will be verified henceforth.
💡
to be done: provide illustrative examples of code