Re: Formal methods

[Paul Rubin <no.email@nospam.invalid>]

Simon Wright <simon@pushface.org> writes:
> This demonstrates to me that I will never be competent at SPARK.
> https://stackoverflow.com/a/66788892/40851

There is some further discussion of those techniques here:

https://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_investigate_unproved_checks.html

I remember a more tutorial document from a while back, but can't easily
find it right now.  It showed an example of a Coq proof connected up to
SPARK.

It probably helps to have studied some basic mathematical logic (proof
theory) before getting into this SPARK stuff.  That makes it flow fairly
naturally.