From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) 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.6
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: Adacore joins with Ferrous Systems to support Rust
Date: Thu, 03 Feb 2022 21:19:14 -0800
Organization: A noiseless patient Spider
Message-ID: <87ee4jxl7x.fsf@nightsong.com>
References: <87o83pzlvm.fsf@nightsong.com> <stdvgv$76k$1@gioia.aioe.org>
	<87bkzpyqx3.fsf@nightsong.com> <stfbf5$bvi$1@gioia.aioe.org>
	<8735l0zo6j.fsf@nightsong.com> <stfg0v$1luk$1@gioia.aioe.org>
	<87v8xwy3y7.fsf@nightsong.com> <sti739$pe4$1@franka.jacob-sparre.dk>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org; posting-host="0725112b9ebf3dc4793d02668cc0208c";
	logging-data="3180"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18fddlgiSMqzSfsxLxFxyfY"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.1 (gnu/linux)
Cancel-Lock: sha1:q2nBN7Ft/7FRckT6d0FWxUWr1DY=
	sha1:CB45U/7L7GNIZs0/xtpfuF2qmeY=
Xref: reader02.eternal-september.org comp.lang.ada:63471
List-Id: <comp.lang.ada>

"Randy Brukardt" <randy@rrsoftware.com> writes:
> In any language with dynamic checks, one can easily reduce the problem
> of correctness down to simply proving that no check fails.

Well sure, but I'd take issue with the word "easily" there.  The
invariants for the red-black tree are fairly complicated.  Enforcing
them could be done with what I think SPARK calls a "ghost function" or
something like that: a piece of code that is not actually executed, but
is used only by the prover.  But, what would the proof look like?  I
think it would likely involve some manual work with an external proof
assistant like ISABELLE.  That takes quite a bit of effort and knowledge
on the programmer's part.

On the other hand, the RB tree type declaration in that Haskell example
is very natural and appealing even in that old implementation, and using
newer GHC features that have appeared since then, it becomes even nicer.

> So the question is how one can accomplish that with the least
> complication for the actual programmer.

Indeed.