AdaCore Blog

RFCs for Ada and SPARK evolution now on GitHub

by Yannick Moy , Raphaël Amiard , Tucker Taft

Ever wished that Ada was more this and less that? Or that SPARK had such-and-such feature for specifying your programs? Then you're not alone. The Ada-Comment mailing list is one venue for Ada language discussions, but many of us at AdaCore have felt the need for a more open discussion and prototyping of what goes in the Ada and SPARK languages. That's the main reason why we've set up a platform to collect, discuss and process language evolution proposals for Ada and SPARK. The platform is hosted on GitHub, and uses GitHub built-in mechanisms to allow people to propose fixes or evolutions for Ada & SPARK,or give feedback on proposed evolutions.

For SPARK, the collaboration between Altran and AdaCore allowed us to completely redesign the language as a large subset of Ada, including now object orientation (added in 2015), concurrency (added in 2016) and even pointers (now available!), but we're reaching the point where catching up with Ada cannot lead us much further, and we need a broader involvement from users to inform our strategic decisions.

Regarding Ada, the language evolution has always been a collective effort by an international committee, but here too we feel that more user involvement would be beneficial to drive future evolution, including for the upcoming Ada 202X version. Note that there is no guarantee that changes discussed and eventually prototyped & implemented will ever make it into the Ada standard, even though AdaCore will do its best to collaborate with the Ada Rapporteur Group (ARG).

You will see that we've started using the RFC process internally. That's just the beginning. We plan to use this platform much more broadly within AdaCore and the Ada community to evolve Ada and SPARK in the future. Please join us in that collective effort if you are interested!

Posted in #Ada    #SPARK   

About Yannick Moy

Yannick Moy

Yannick Moy is SPARK Product Manager at AdaCore and co-director of the ProofInUse joint laboratory with Inria. At AdaCore, he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick leads the developments of SPARK, a product he presents in articles, conferences, classes and blogs (in particular Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.

About Raphaël Amiard

Raphaël Amiard

Raphaël Amiard is a software engineer at AdaCore working on tooling and compiler technologies. He joined AdaCore in 2013, after an internship on AdaCore's IDEs. His main interests are compiler technologies, language design, and sound/music making.

About Tucker Taft

Tucker Taft

S. Tucker Taft is VP and Director of Language Research at AdaCore, a company focused on open-source tools to support the development of high-integrity software. Tucker joined AdaCore in 2011 as part of a merger with SofCheck, a company he had founded in 2002 to develop advanced static analysis technology. Prior to that Tucker was a Chief Scientist at Intermetrics, Inc. and its follow-ons for 22 years, where in 1990-1995 he led the design of Ada 95. Tucker received an A.B. Summa Cum Laude degree from Harvard University, where he has more recently taught compiler construction and programming language design.