Re: value-flavoured structures

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.