-------- Original Message --------

>     Eh, my knowledge of Ada is dated. I wrote a lot of wrappers of Linux
> syscalls and IOCTLS. It was actually a delightfull job to create clear, simple,
> and safe interfaces to some complicated, tricky, and dangerous IOCTLS of the VME
> driver.

I'm sure that is all still true as Ada is a very stable language and most of Ada
except for some high level more magical abilities are available in SPARK :-).
There may be a number of warnings about assumptions made about the C interface
that the engineer will hopefully consider at some point. I have more experience
on volatile variable use and bare metal where you have to make seemingly
insignificant changes to ensure you avoid potential side affects.

https://www.adacore.com/blog/formal-proof-on-device-drivers-with-spark

> But this was before the advent of SPARK.

I know what you mean as in SPARK has been getting much easier to use in recent
years but surprisingly SPARK is as old as Ada if not older, atleast as a goal
(The wikipedia page says 86 but I have a book at home that talks about the
foundations being formed in the 70s in the Royal Navy). It's called SPARK 2014
and I guess it has an often updated manual but isn't standardised in the same
way as Ada.

Updated in 2026, in fact.

https://docs.adacore.com/spark2014-docs/html/ug/

-- 
All the best,
             Kevin Chadwick