Ada and SPARK - with Alexander Senier

Show Notes and Links

Flo and Julian talk to Alexander Senier about Ada, SPARK and how to build reliable and trustworthy software. We also talk about Alexander’s company, Componolit.

• Discuss the episode in Matrix room #ukvly:matrix.org or on Freenode IRC #ukvly.
• Send feedback to [email protected] or via Twitter.

Resources to get started

• awesome Ada: A curated list of awesome resources related to the Ada and SPARK programming language.
• learn.adacore.com
• Free book: Safe and Secure Software - An invitation to Ada 2012
• Implementation Guidance for the Adoption of SPARK
• John W. McCormick, Peter C. Chapin: Building High Integrity Applications with SPARK
• Ada for the C++ or Java Developer
• Rust and SPARK: Reliability for Everyone (the statements on SPARK pointers are outdated!)
• Alire: the Ada package manager
• Ada Devevelopers room at FOSDEM

Low-level and systems programming resources

• Ada Bare Bones
• Spunky: A kernel using Ada
• Ada drivers library
• Ada Operating System development example

Resources specific to component-based systems

• Genode has built-in support for SPARK/Ada
• Muen, a separation kernel fully implemented in SPARK
• Ewok, a microkernel for embedded systems implemented in SPARK
• Gneiss - framework for platform-independent SPARK components running on Genode, Muen and Linux
• RecordFlux - Verifiable message parser/generators in SPARK
• Article: SPARK as an extremum: Components in pure SPARK