Return to Activities

Bug-free Coding with SPARK Ada

Learn to write maintainable bug-free code with SPARK Ada.

Workshop Overview

  • Beginner
  • 1.5h - 2h
  • SPARK, Ada

Learning Objectives

  • Setting up SPARK Ada on your computer
  • Building a stack data structure
  • Using SPARK tools find bugs in your code

Have a question?

Get in touch if you have any questions regarding this workshop or MLH Localhost.

About this Workshop

During this workshop, you’ll teach participants what makes the Ada programming language special and why they should use it, how to write bug-free code with SPARK Ada and how to implement the stack data structure in SPARK Ada.

Build with Ada

Ada is a general purpose, modern programming language like Java, C, and C++. It was created in the 1980s for the United States’s Department of Defense. Ada is an excellent choice if you’re writing code for embedded systems, applications that will have a long life-span, or where human lives are at stake.

Bug-free code with SPARK

SPARK is a subset of the Ada programming language that does program verification. It checks for syntax errors, run-time errors, and proof of properties. This means that your code is bug-free before you deploy it.

Requirements / Prerequisites

Participants will be required to have a computer that can connect to the Internet and a web browser.

While there are no formal prerequisites for this workshop, participants will benefit from some experience with languages such as Java, C, and C++.


When you host an MLH Localhost activity, we’ll send you everything you need to run it. Here’s what we’ll send you:

The List:

Resources & Downloads

Participants will access SPARK Ada through Adacore's iteractive learning platform, Learn Ada

Get Started

The hackers are waiting for you.

Have a question?