Why I plan to use SPARK everywhere

I think I understand all the other points but isn’t Ada.Unchecked_Conversion a generic library.

Do you mean it can’t be expanded upon like tagged extension?

I’m not sure what you mean. Streams, particularly useful for tagged types looks easy enough to implement for a light runtime (assuming there isn’t underlying machinery which isn’t missing to save space). However for untagged records it just looks like more work and more error prone due to ordering than unchecked_conversion atleast where endianness is known to always be little.

1 Like

Unchecked_Conversion is not a library and not generic. It is a built-in language feature shaped as a generic. The design could be different, e.g. and attribute. Normal type conversion is not generic though it has exactly same functionality.

I guess that the choice was to scare programmers off like in the case of Unchecked_Deallocation.

How is it (streams) related to usability of X’Valid?