Why SPARK83 over SPARK2014?

[rod-chapman]

May I ask... why did you choose to implement this in SPARK83 rather than SPARK2014?
Are you committed to using an Ada83 or Ada95 compiler perhaps?

[lkujaw]

Hello,

Thank you for your question, it is quite exciting to hear from you. My aim was to attempt to support the widest variety of platforms possible. While I am sure there are considerably fewer users these days, I believe the DEC Ada and Janus compilers (for real-mode PC DOS) are still commercially supported to some degree. Another factor is my familiarity with the Isabelle proof assistant and its integration with the annotation-based SPARK toolset, which has been quite helpful in modeling the properties of modular arithmetic and bit manipulations. I hope this clarifies the context behind my choice, and I would to add that I am very grateful for the continued evolution of SPARK and the increasing scope of the Ada language that is now amenable to proof.

As an aside, I was wondering if you might be able to help me with a SPARK-related question. The testing program I provide (which is not part of the ALIRE crates) uses a customized version of the SPARK_IO package. I recently came across the same within the Tokeneer package but featuring a U.S. government copyright notice. Do you know if it is acceptable to distribute SPARK_IO as part of an MIT-licensed open source package, and if so, how may I properly provide attribution?

Thank you so much for your involvement with the development of the SPARK language. I have found working with the SPARK toolset to be quite rewarding; the BLAKE2s package certainly owes much of its quality to the proofs facilitated by it.

Kind regards, Lev

[lkujaw]

I've added the following rationale (58431ac) to the project README regarding the choice of SPARK83:

"For the 1987, 1995, and 2007 editions of the ISO Ada standard, the corresponding SPARK language tools were based upon annotations. The placement of annotations within Ada comments has the advantage of not requiring any special support for SPARK on the part of the compiler.

At the time of writing, the compiler support required by the post-2007 editions of the SPARK language is found only within the GNAT compiler. Like the BLAKE2s reference source code, which targets the first edition of the ISO C standard released in 1990, this project targets the earliest release of the ISO Ada standard to maximize portability, and for this same reason the annotation-based SPARK language tools are ideal."

Please let me know if this language adequately addresses your inquiry (via closing this issue) or how I can improve it.

Thank you, Lev

[rod-chapman]

It would be good to know exactly which compilers you have build and tested it with... e.g. GNAT Community 2020 or 2021 (with which operating systems? Linux, Windows, MacOS? Any embedded/cross targets?) or perhaps with the FSF GNAT release that is now in Alire?