Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.forth
Subject: Re: value-flavoured structures
Date: Sat, 28 Sep 2024 11:06:52 -0700
Organization: A noiseless patient Spider
Lines: 15
Message-ID: <87ldzbd54z.fsf@nightsong.com>
References: <nnd$61e0ad9a$48ed61c2@b4d945e456041481>
	<c54d153e547438fb9f033b35b270f7cf@www.novabbs.com>
	<vd710j$mrev$2@dont-email.me> <87zfnscypb.fsf@nightsong.com>
	<nnd$61138f06$6ebe7c5e@dd9a69aae34886e2>
	<87plond5te.fsf@nightsong.com>
MIME-Version: 1.0
Content-Type: text/plain
Injection-Date: Sat, 28 Sep 2024 20:06:53 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="267fe6ba0f2707ae3557a9250710d2a6";
	logging-data="1435802"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1/6Tx/tOeRs0iv93ur3IEUw"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.1 (gnu/linux)
Cancel-Lock: sha1:wJYWMfI0+2DnEnWbF4KRv1b7ygc=
	sha1:dL0bhNcDQ557nwE1AE1XBTFvIdk=
Bytes: 1840

Paul Rubin <no.email@nospam.invalid> writes:
> Rust has unsafe modules but I don't remember Ada having them.  Ada does
> have an Unchecked_Conversion function but I don't know where this is
> really needed or how well specified it is in the language standard.

Added: Ada also has "overlays" so you can make two objects share the
same machine address, ouch!  

https://en.wikibooks.org/wiki/Ada_Programming/Type_System#Overlays

It would surprise me if SPARK allows this feature, and it also might not
allow Unchecked_Conversion.  SPARK is an Ada subset that is supposed to
be extremely safe, and it allows a lot of static verification.  I've
been wanting to try it.  It is designed for use in critical embedded
systems.