Blog
An Insight Into the AdaCore Ecosystem
Formal Methods Practice and Theory
Quentin Ochem
Announcing Publication of the Draft Ferrocene Language Specification
We are pleased to announce the publication of the initial draft of the Ferrocene Language Specification (FLS) - a qualification-oriented document…
Fabien Chouteau
Announcing The 2022 Ada/SPARK Crate Of The Year Award
We're happy to announce our the second edition of our programming competition, the Ada/SPARK Crate Of The Year Award! We believe the Alire package…
Yannick Moy, Lionel Matias
I can’t believe that I can prove that it can sort
When an enthusiastic Ada programmer and a SPARK expert pair up to prove the most "stupid" sorting algorithm, lessons are learned! Join us in this…
Fabien Chouteau
A New Era For Ada/SPARK Open Source Community
Today we have two exciting announcements for the future of the Ada/SPARK ecosystem.
Gustavo A. Hoffmann
Announcing Updates to learn.adacore.com
Paul Jarrett
Ada Crate of the Year: Interactive code search
A retrospective on learning Ada and developing a tool with it in 2021 from 2021 Ada Crate of the Year Winner Paul Jarrett.
Claire Dross
Handling Aliasing through Pointers in SPARK
Fabien Chouteau, Joffrey Huguet
Quite Proved Image Format
A few weeks ago a piece of code went viral in the online dev community. The “Quite OK Image Format” (QOI) is a fast, lossless image compression…
Fabien Chouteau
Ada GameDev Part 2: Making 2D maps with Tiled
In this second post of the Ada GameDev series we will see how to create game maps and export them to a format that is compatible with the GESTE…
Manuel Hatzl
SPARK Crate of the Year: Unbounded containers in SPARK
Manuel Hatzl is the winner of the 2021 SPARK Crate of the year! In this blog post he shares his experience using Ada/SPARK and how he created the…
Fabien Chouteau
Ada GameDev Part 1: GEneric Sprite and Tile Engine (GESTE)
In this first entry of the series, I want to present my GEneric Sprite and Tile Engine (GESTE) project. The goal of GESTE is to bring the rendering…
Yannick Moy, Claire Dross
Proving the Correctness of GNAT Light Runtime Library
The GNAT light runtime library is a version of the runtime library targeted at embedded platforms and certification, which has been certified for use…