Ada SPARK Office Hours

The Ada SPARK Office Hours is an initiative that we started in June this year. Our goal is to create an open-mic atmosphere where professionals, hobbyists, students, and enthusiasts can come together to discuss Ada SPARK, share their hobby projects, what they could use help with, what is working, what is not, what could be improved, and any other topic related to Ada SPARK.

Ada SPARK Office Hours are held every second Friday at 10 am Eastern Time; the link to the calendar invite is on the AdaCore website. Sessions are recorded and available on the Ada Forum Event page, complete with summaries. There is also a YouTube playlist.

Many topics have been discussed; one of the top topics has certainly been the use of Artificial Intelligence to generate Ada SPARK code and to lift code to SPARK Silver to prove the absence of runtime errors. As many people in the meetings have concluded, Large Language Models are good at adding invariants and assertions that help prove the code. The commercial models are leading the pack, but the open weight models are improving rapidly as well. The formal methods underlying Ada SPARK help build trust in the AI-generated output.

AdaCore has released a number of LLM Skills that can help with various Ada-related tasks and tools.

We also spoke about Ada for Embedded and about how to develop scalable device models. There are a couple of approaches available, and there is strong interest in improving the available runtimes and crates, as well as the documentation. Ada can run bare-board, directly on the hardware, on Linux, RTOSes, or on Zephyr.

Lastly, there was a session on how to approach formal verification, where to get started, and how to get your hands dirty.

In general, the event is a great opportunity to share your ideas and learn from others in the community. We hope to continue with the event over the next months, and we hope to encourage students to join as well, as the academic year is starting soon.