Specifications Matter: The Case for SPARK in the…

What to teach students when the code writes itself

Every computer science and engineering department is currently having the same argument. Students arrive able to produce working code on day one, because an LLM produces it for them. The traditional curriculum of teaching them to program by covering syntax, loops, data structures, pointers, linked lists, and the like no longer discriminates between students who understand and those who do not, because both submit code that runs.

You can police it, ignore it, or lean in. I argue for a fourth: change what you assess. The production of implementations is now cheap, and software development is being democratized. Instead, grade the production of specifications and the judgment of whether an implementation satisfies one. That is a teachable skill; it differentiates students in the real world. The technology is readily accessible, and there is real demand for these skills in the market.

That toolchain is SPARK.

Evolution, not revolution

Let me be precise about what I am proposing. I am not proposing to change the entire curriculum. We still need students to understand the syntax, how memory works, and how to put a linked list together, for now, at least.

I am not proposing an Ada-first curriculum. I am not proposing that SPARK replace Python in CS1. I am proposing a three-to-four-week module within an existing course — software engineering, programming languages, formal methods, or an embedded systems elective — in which students write contracts and a prover unambiguously tells them whether their code satisfies them.

That is a small enough ask to actually happen, and it is sufficient to make a difference in how students view software engineering and to prepare them for the agentic, AI-driven times ahead.

Now, there may already be a module in the curriculum that covers formal methods. SPARK is different, though; it is the only language in which the formal methodology is incorporated into the language. This blog post provides pointers for educators to help them refresh or revitalize the computer science and engineering curriculum, especially in light of the availability of artificial intelligence.

What the module gives students that nothing else does

Students meet correctness in three forms today: testing, code review, and, in the fortunate case, a formal methods course taught with pencil and paper. The latter was the case for my education; my curriculum had no space for Java, C, C++, and Python was only just released.

Testing teaches that correctness is sampled. In the words of Edsgar Dijkstra: “Program testing can be used to show the presence of bugs, but never to show their absence!”¹

Review teaches that correctness is a matter of an experienced person's opinion. Pencil-and-paper formal methods teach that correctness is provable in principle, but expensive and detached from anything they will ship.

SPARK teaches something different: correctness as a property you state precisely, and a machine decides, on real code, for all execution paths. A student writes a precondition and a postcondition, GNATprove either discharges the verification conditions or reports exactly which one it cannot discharge. The feedback loop is fast, rigorous, and helpful for the programmer in understanding what may be wrong.

Two things follow that are hard to get any other way.

The first is that the specification becomes visible as a distinct artifact. Most graduates have never written one. They have written code and, if pressed, a docstring. Asking a student to state what a subprogram guarantees for all inputs and then watching a prover reject their first three attempts because the statement was too weak, or vacuous, or quietly assumed something the caller cannot provide — teaches precision in a way that no marking rubric can. And in SPARK, that specification is in the program itself in the same syntax as the program. Intrinsically integrated and interwoven.

The second is that the student learns the ‘why’ of a mistake. When a proof fails, it fails at a specific verification condition. The prover states which claim does not hold, and the student can dig in. That is a much better teacher than a failing test case, because it points at the reasoning rather than the symptom.

Both of these are, not incidentally, exactly what a working engineer now needs to supervise generated code.

Evidence of the Benefit of Ada and SPARK

Evidence of the benefit of one language over another is hard to come by. It would require randomized, blind comparisons of multiple implementations of the same set of requirements.

Nonetheless, there are three distinct case studies that we can point to in this space.

John McCormick taught a real-time systems course for over twenty years, in which undergraduate teams built the same 10–15K-line multitasking embedded system — a model railroad controller, device drivers, and scheduling logic — in a single fifteen-week semester. Teams implemented it in both Ada and C, and he published the comparison in Ada User Journal 29(3), 2008². The headline finding is that the language materially changed what students could complete in the time available: the teams working in a language whose toolchain rejected whole classes of error at build time spent their semester on design, while the others spent it on defects.
This is a limited study. A single instructor, a single institution, non-randomized, and published in the Ada community's own journal by a self-identified advocate. It is not a controlled trial by any means, but it is a valid data point.
NVIDIA presented the benefits of using SPARK at several DEFCON conferences. The study reports that up to 70% of memory safety issues are found during security testing of traditional C and C++ code, and that projects written in Ada SPARK can achieve 50% to 70% defect reductions.³
A VDC study on software quality and the benefits that memory-safe languages provide, citing lower development costs, reduced time-to-market, and increased focus on innovation.⁴

What these proof points establish is a mechanism worth taking seriously — that shifting error detection earlier does not merely reduce bugs, it reallocates the programmer/students' scarcest resource toward the work that requires thinking.

When applied in a fifteen-week course, that reallocation is the difference between a project that teaches design and one that teaches debugging.

For the broader course-design literature, see also Tempelmeier's account of running a programming-languages course with Ada (Ada-Europe 2012, LNCS 7308)⁵, and McCormick, Singhoff and Hugues, Building Parallel, Embedded, and Real-Time Applications with Ada (Cambridge UP, 2011)⁶, which is written at an undergraduate level and is the obvious textbook if the module grows into a course.

The four objections

The number of programmers using Ada and SPARK is small compared with more established languages such as C, C++, Rust, Python, and others, as the TIOBE index clearly indicates. So when we propose increasing the amount of Ada and SPARK in university curricula, we often face one or more of four objections.

"It won't help them get a job."
The honest answer is that SPARK is a niche skill with concentrated demand — avionics, rail, space, defense, automotive, medical devices, and increasingly security-critical infrastructure. It is not a general employability play, and pretending otherwise damages credibility with students.
SPARK teaches transferable skills, not syntax, much like C teaches understanding of memory management. For SPARK, it is the habit of stating invariants and reasoning about them, which shows up in Rust's type system, property-based testing, database constraints, API contract design, and — the reason this is urgent now — in reviewing generated code. Students who have had a prover reject their sloppy postcondition are better at all of these.
Especially going forward in the world of LLMs and agentic AI, the language is not the challenge; the thinking process is, and this is where SPARK excels and teaches students something no other language can.
"There's no room in the curriculum."
There is, because something in the existing course is now worth less than it was. The two-week block on implementing standard data structures by hand no longer assesses much. Trade it.
"Our faculty don't know SPARK."
This is a real constraint. Adopting the module requires a member of staff to spend several weeks preparing. What reduces that cost? AdaCore's learn.adacore.com provides a browser-based, interactive course with exercises that run without any local install, removing both the faculty ramp-up problem and the first-week toolchain support burden that kills so many module adoptions. Ada-Europe's conference has a standing education track, and there is an existing community of academics who run these courses and, in my experience, are unusually willing to share material.
AdaCore has a well-respected GNAT Academic Program (GAP)⁷ to help universities incorporate Ada and SPARK into their curricula. The GAP team at AdaCore can share content, best practices, and generally brainstorm the approach.
Lastly, much of the content needed for a curriculum is published in a series of videos, each around 30 minutes or less, on AdaCore University's YouTube channel.
"The tooling will cost us."
It does not. GNAT is FSF-licensed and ships with standard distributions; the SPARK toolset is available under terms that cover academic use.

A concrete four-week module

Here is a short, four-week module, written to be dropped into an existing second- or third-year software engineering course.

Week 1 — Types as specifications. Ada's scalar and subtype model. Constraining a value's range at the type level; what becomes unrepresentable rather than merely untested. Students refactor a small program so that a class of bugs cannot be written.
Week 2 — Contracts. Preconditions and postconditions on subprograms. Students specify before implementing. First encounter with a vacuous or too-weak postcondition that proves nothing, and the discussion that follows is the most valuable hour of the module.
Week 3 — Proof, and what it does not cover. Running GNATprove. Reading a failed verification condition. Loop invariants. Crucially: the boundaries of the guarantee — what the prover assumes, what it says nothing about, why you still need tests.
Week 4 — Generated code under a specification. Students write the contract; an LLM model writes the body; the prover adjudicates. Assess the quality of the specification and the student's written account of whether the generated implementation satisfied it.

Week 4 is the one that delivers the differentiation, and it is also the one that will most interest a curriculum committee, because it is a defensible answer to a problem every department has right now. The students will also appreciate weeks 1-3, as they teach them a different way of thinking about algorithms, types, ranges, and proper software engineering techniques. This is the feedback that comes back from practitioners who have gone down this path.

Summary

I am proposing a new insert in the existing computer science or engineering curriculum. A module that differentiates students from others in the market. It teaches them formal methods in a practical way, supported by a modern programming language. The reasoning that this module teaches them will stick with them throughout their career. It will elevate their software development capability. It will also prepare them for changes in the industry, as software will increasingly be generated by AI and LLMs, with specifications defining it.

SPARK is an elegant language, memory-safe, strongly type-safe, and enabling incremental checking. AdaCore is here to support educators who want to go down this path. Have a look at the resources in this blog post and reach out to the GNAT Academic Program, or attend one of the bi-weekly Ada SPARK Office Hours⁸.

¹_{EW Dijkstra, Notes on Structured Programming, section 3,}_{https://www.cs.utexas.edu/~EWD/ewd02xx/EWD249.PDF}

²_{McCormick, J. W. (2008). "Ada and Software Engineering Education: One Professor's Experiences." Ada User Journal 29(3), 203–207. Free full text:}_{https://www.ada-europe.org/archive/auj/auj-29-3.pdf}

³_{When Formal Verification with SPARK is the Strongest Link,}_{https://www.adacore.com/blog/when-formal-verification-with-spark-is-the-strongest-link}

⁴_{Memory-Safe Languages Offer Protection for Devices and TCO,}_{https://www.adacore.com/papers/memory-safe-languages-offer-protection-for-devices-and-tco?utm_source=linkedin&utm_medium=organic+social}

⁵_{https://link.springer.com/book/10.1007/978-3-642-30598-6}

⁶_{https://www.cambridge.org/core/books/building-parallel-embedded-and-realtime-applications-with-ada/9FC78A90F1B6A2228D69E32CE610A66C}

⁷_{GNAT Academic Program -}_{https://www.adacore.com/acadeAssessmia}

⁸_{Ada SPARK Office Hours -}_{https://www.adacore.com/ada-spark-office-hours}