From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.5-pre1 (2020-06-20) on
	ip-172-31-74-118.ec2.internal
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=3.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.5-pre1
Path: eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Formal methods
Date: Thu, 25 Mar 2021 15:29:15 -0700
Organization: A noiseless patient Spider
Message-ID: <87wnturhok.fsf@nightsong.com>
References: <ly35wij2vt.fsf@pushface.org>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org; posting-host="835598ae6c6981d3d35b1665ade1362a";
	logging-data="12437"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+LzKSJOkoOkW3d+5CfPbhl"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (gnu/linux)
Cancel-Lock: sha1:KOSw2+nvbpYH8lu8cHTreh3m5/Q=
	sha1:OLvLh6lVWm/O0+7rLY0H+o8cTtw=
Xref: reader02.eternal-september.org comp.lang.ada:61655
List-Id: <comp.lang.ada>

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.