SPARK (Pro 25)

This assessment applies the coupling account — coupling as access to a shared resource, and the coupling floor [1], [2] — and the knowledge-embodiment theorem [3]; the language is assessed against its official reference [4].

1 Assessment

This page assesses SPARK in five parts: core coupling — what the language’s own constructs force; ecosystem coupling — what the surrounding platform, tooling, and community cost; engineering readiness — whether the artifact can be reproduced, verified, observed, worked in quickly, connected to other languages, and governed openly; the profile — the unscored facts a score cannot express; and the scoring detail — the mechanism marks and the arithmetic behind every score. A ✅ bullet marks a construct that helps. A ⚠️ or ❌ bullet marks a cost; the scoring model does not price every cost named here.

Core coupling 73/100 · Ecosystem coupling 69/100 · Engineering readiness 42/100

1.1 Core coupling

1.1.1 Type

  • ✅ The static type system is Ada’s: Every object, parameter, and function result has a declared type, and the compiler checks every assignment and call
  • ✅ Subtypes carry range constraints: subtype narrows a base type with a range or a predicate, and in the proved subset a violation is a proof obligation rather than a run-time check
  • ✅ Enumeration and discriminated record types express alternatives: An enumeration gives a finite value set, and a variant record’s discriminant states which branch is active
  • ✅ Generics are checked at each instantiation: An Ada generic is analysed where it is instantiated, so a reusable abstraction is verified at its use site
  • ✅ Type_Invariant states a property of a private type: The invariant is an obligation on every value of the type
  • ⚠️ Access types are admitted only under an ownership policy: SPARK allows a pointer when its owner is declared, so indirection is available but constrained

1.1.2 Construction

  • ✅ Contracts are part of the subprogram declaration: Pre, Post, and Contract_Cases state the obligation beside the parameters, so a caller reads it with the signature
  • ✅ Flow contracts state what a subprogram reads and writes: Global, Depends, and Refined_Global make the data flow a declared artefact
  • ✅ Abstract states confine a package’s state: Abstract_State declares the state as an abstraction, Refined_State binds it to concrete variables, and Initializes states what a package sets up
  • ✅ Separation is proved rather than advised: The ownership policy, the flow aspects, and the contracts are analysed by GNATprove, so a declared separation is verified and not merely recommended
  • ⚠️ The declarations carry more than the code needs: A proof requires a contract for every subprogram on the path, so construction carries an annotation burden
  • ⚠️ A unit can opt out with SPARK_Mode => Off: An analysed region and an unchecked region can sit in the same program

1.1.3 Memory

  • ✅ An ownership policy governs any access type: SPARK’s data-ownership regime gives a pointer a stated owner, so a dangling or duplicated reference is a proof failure rather than a run-time defect
  • ✅ No manual deallocation in the subset: Unchecked_Deallocation is outside SPARK, so a program never frees memory by hand
  • ✅ No garbage collector: SPARK compiles to native code and runs without a collector
  • ✅ Bounded containers remove the heap: Ada.Containers.Bounded_Vectors and its siblings hold their storage in the object
  • ✅ A local object’s lifetime is its scope: A stack variable’s extent is fixed by the block that declares it
  • ⚠️ An owned access type still allocates at run time: The allocation is allowed and proved, but the allocator’s behaviour remains a run-time fact

1.1.4 Error

  • ✅ A failure is a proof obligation: GNATprove reports an unproved check, so a fault is found in the toolchain rather than in a test run
  • ✅ A raise is stated in the contract: Exceptional_Cases names the exceptions a subprogram may propagate, so the failure set is declared
  • ✅ Run-time checks are proved impossible rather than disabled: Once GNATprove proves that an index, a range, or a division cannot fail, the check costs nothing
  • ✅ Assert becomes a proof obligation: pragma Assert states a property that the analysis must establish or report
  • ✅ Assume records an unproved fact explicitly: An assumption is written in the source and appears in the analysis report
  • ⚠️ The proof is no stronger than its assumptions: An Assume, an unproved check, or a SPARK_Mode => Off unit leaves a gap in the guarantee

1.1.5 Concurrency

  • ✅ Ada tasking is available and analysable: A task and a protected object are language constructs, and SPARK analyses the data flow of the supported subset
  • ✅ A protected object is the synchronisation boundary: A protected operation enforces mutual exclusion and a barrier, so the lock is not written by hand
  • ✅ The Ravenscar profile gives a static task set: No task is created dynamically, and the ceiling-locking protocol prevents priority inversion
  • ✅ Shared state must be declared: A variable shared between tasks appears in a Global or Depends aspect, so the sharing is visible
  • ⚠️ The analysed subset of tasking is smaller than Ada’s: An entry family, a dynamic rendezvous, or an unrestricted task is outside the analysed subset

1.1.6 Platform

  • ❌ SPARK is a subset of Ada and a program is an Ada program: GNAT compiles the code, and the language has no existence apart from the Ada platform (P1)
  • ❌ A foreign call leaves the proved region: An interface to C or another language is declared outside SPARK, so it cannot be analysed with the rest
  • ✅ GNAT is a mature and portable Ada compiler: The same source compiles for x86-64, ARM, and the embedded targets used in avionics
  • ✅ The qualified toolchain targets the certificated platforms: GNAT Pro supports VxWorks, LynxOS-178, and bare metal with a qualification for DO-178C
  • ⚠️ Full support is a commercial subscription: GNATprove is available in the community toolchain, and SPARK Pro adds support, libraries, and qualification
  • ⚠️ The build is a GNAT project: gprbuild and a project file describe the build, so the project couples to the Ada toolchain

1.1.7 Trade-offs (not coupling)

  • The proved subset is smaller than Ada: A feature outside SPARK is left out or isolated behind a SPARK_Mode => Off boundary
  • The restriction on pointers is a deliberate exchange: Aliasing is removed in return for an ownership regime and an array or a bounded container in place of a linked structure
  • The annotation burden is the price of the proof: A contract, an invariant, and a flow aspect are written for each unit on the path
  • The target domain is high-assurance by design: Aviation, space, and medical devices are the intended context, and the domain mark records that scope
  • Verification effort is a project decision: Zero-defect software is achievable given sufficient effort, which is a budget choice
  • The proof checks the contract, not the requirement: A verified program can implement the wrong specification, which no toolchain detects

1.2 Ecosystem coupling

1.2.1 Performance

  • ✅ The compiled output is an Ada program’s native binary: SPARK compiles to the same native code, so the verification adds no run-time cost
  • ✅ A proved check need not execute: A check that GNATprove established can be suppressed at that point, so the verified code does not pay for the guard
  • ✅ No collector and no interpreter: The run-time has neither a garbage collector nor a JIT, so the timing is the Ada run-time’s
  • ✅ The Ravenscar profile bounds the run-time behaviour: The task set, the priorities, and the locking are static, which makes the timing analysable
  • ⚠️ The run-time is the Ada run-time: Tasking, the secondary stack, and exception propagation cost what GNAT’s run-time costs
  • ⚠️ The proof is a build-time cost: GNATprove can take far longer than the compilation, which delays the build but not the program

1.2.2 Ecosystem

  • ❌ The SPARK ecosystem is a subset of Ada’s: A library must itself be in the SPARK subset to be analysed with the program (Ec3)
  • ✅ Ada’s tooling serves the project: Alire supplies packages and gprbuild builds the project
  • ✅ GNATprove and SPARK Pro are purpose-built and mature: The analyser and the commercial support layer are actively developed
  • ✅ The industrial community sustains the toolchain: The requirements of the certificated industries drive the analyser and the library work
  • ✅ A verified library base exists: SPARK’s own libraries and verified components ship with the toolchain
  • ⚠️ A library that uses pointers must be isolated: An Ada library outside the subset is reached through an unproved boundary

1.2.3 Evolution

  • ✅ SPARK tracks a published Ada standard: The subset is defined against Ada 2012 and Ada 2022, so a language change follows the standard revision
  • ✅ Successive SPARK releases widened the subset: The ownership policy, the functional contracts, and the proof of type invariants were added over several releases
  • ✅ Ada’s compatibility record is strong: An older Ada program generally compiles under a later revision
  • ⚠️ A new feature arrives with a toolchain release: The analyser states the subset it supports, so adoption follows the release
  • ⚠️ A proof depends on the toolchain version: A check proved under one GNATprove release can need a new annotation under another

1.2.4 Domain

  • ❌ The language exists for high-assurance systems: Aviation, space, and medical devices, where DO-178C, EN 50128, or IEC 62304 applies, are the intended domains (D1)
  • ❌ Outside those domains it is rarely chosen: A general application gains little from the proof and pays the toolchain cost (D1)
  • ✅ The fit in the intended domain is excellent: The tools, the libraries, and the certification evidence all target it
  • ✅ DO-333 credits the proof against the certification objectives: The formal-methods supplement to DO-178C lets the analysis substitute for some test objectives
  • ✅ The shipping uses are real: Airbus, Thales, and Lockheed Martin build critical software on it
  • ⚠️ The labour pool is small: An engineer with both Ada and formal-methods experience is hard to find

1.2.5 Learning

  • ❌ Two skills must be learned, not one: SPARK requires Ada fluency and formal-methods practice, so contracts, invariants, and the proof tool must all be mastered (L1)
  • ❌ A proof failure must be read as a counterexample: GNATprove reports an unproved check with a path, and turning the report into a fix takes experience
  • ✅ The analysis report is actionable: The tool names the check, the path, and the assumption that blocks the proof
  • ✅ The learning material is complete: AdaCore’s tutorial and the SPARK course material cover the language and the proof method
  • ⚠️ The learning curve is very steep: A first proved subprogram is quick to write, and a first proved package with an abstract state is not

1.2.6 Syntax

  • ✅ The syntax is Ada’s: A package, a subprogram, and a loop read as they do in Ada, and a contract appears as an aspect or a pragma
  • ✅ The block structure is explicit: A begin/end pair closes a block, and the end repeats the name it closes
  • ✅ Contracts sit beside the parameters: Pre =>, Post =>, and Global => are part of the subprogram declaration
  • ✅ Quantified expressions are first-class: (for all I in A'Range => A (I) > 0) states a property in the source
  • ⚠️ An aspect clause can be long: A Depends aspect over much state is a long expression that needs careful reading

1.2.7 Testing

  • ✅ The proof covers the property the contract states: An obligation is discharged for every value it quantifies, not for a sample
  • ✅ The test suite no longer has to trigger every check: A bounds or range check proved impossible needs no test to reach it
  • ✅ gnattest generates a unit-test harness: It reads a package specification and emits AUnit test stubs
  • ✅ AUnit covers the behaviour a contract does not state: The proof and the test suite answer different questions
  • ⚠️ A property that no contract states is not proved: The analysis reaches exactly the contracts and invariants that are written

1.2.8 Security

  • ✅ The classic memory-safety faults are proved absent: A buffer overflow, a use-after-free, and a null dereference are removed by the subset and the proof, so the vulnerability class does not exist in the analysed code
  • ✅ Input validity is stated and checked: A range constraint or a Pre aspect states what the caller must guarantee, and the proof covers the rest
  • ✅ Unchecked_Conversion and pointer arithmetic are outside the subset: The unsafe operations are not available to analysed code
  • ⚠️ The guarantee stops at the SPARK_Mode => Off boundary: An imported C function, a device driver, or an unchecked allocation is not proved
  • ⚠️ The trusted base includes the prover and the compiler: A defect in GNATprove or in the code generator is outside the proof

1.3 Engineering readiness

1.3.1 Reproducibility

  • ❌ Builds are not byte-reproducible by default.
  • ❌ Dependencies resolve without a lock by default.

1.3.2 Supply chain

  • ⚠️ Published packages carry no signed provenance by default.
  • ⚠️ The package registry is a flat name space.

1.3.3 Observability

  • ⚠️ No stable tracing and metrics standard.
  • ⚠️ The standard library has no structured logging.

1.3.4 Feedback

  • ✅ No charged mechanism in this dimension.

1.3.5 Interop

  • ⚠️ No maintained portable target.

1.3.6 Governance

  • ⚠️ One vendor decides the language’s direction.
  • ⚠️ The specification is not public.

1.4 Profile

Unscored, and kept separate from every score on purpose. The profile records what a mechanism price cannot express: what a running program costs, how well a coding model and an agent work in the language, and whether a safety-critical path exists.

1.4.1 Energy and cost

What this axis asks: what does a running program cost in energy and time?

  • ✅ Compiles to native code: the fastest class in the language energy and time benchmarks [5], [6]. A causal re-analysis attributes the difference to execution time [7].

1.4.2 AI and agent readiness

What this axis asks: how well does a coding model and an agent work in this language?

  • ❌ Sparse training data: models write it unreliably [8].

1.4.3 Safety certification

What this axis asks: is there a certified or standards-qualified path to a safety-critical system?

  • ✅ A standards-qualified toolchain or an established safety standard covers this language.

1.5 Scoring detail

1.5.1 Core coupling Dimensions

Dimension Mechanism Description Present Cost
Type T1 dynamic no static check — 0
T2 weak static — 0
T3 dynamic/duck dispatch — 0
T4 no sum types — 0
T5 no generics — 0
T6 no namespaces — 0
T7 type erasure/reflection — 0
T8 operator overloading — 0
T9 inheritance required for polymorphism — 0
T10 no null-safety — 0
T11 no module boundary — 0
T12 no effect tracking ✅ −8
T13 async/sync colouring — 0
T14 unchecked foreign boundary ✅ −4
Type subtotal −12
Construction C1 global mutable state by default — 0
C2 no immutability by default — 0
C3 constructors coupled to allocation — 0
C4 no constructor/validation — 0
Construction subtotal 0
Memory M1 manual deallocation — 0
M2 GC non-deterministic pauses — 0
M3 no RAII — 0
M4 no ownership model — 0
Memory subtotal 0
Error Er1 no structured path — 0
Er2 unchecked exceptions only — 0
Er3 errors ignored/non-exhaustive — 0
Er4 no composable result type — 0
Error subtotal 0
Concurrency K1 GIL/no parallel — 0
K2 shared mutable state default — 0
K3 manual sync no race detection — 0
K4 no structured concurrency — 0
K5 no primitives — 0
Concurrency subtotal 0
Platform P1 cannot function outside one vendor/domain ✅ −15
P2 single-vendor but other uses — 0
P3 legacy/discontinued platform — 0
Platform subtotal −15

Core Dimensions score: 73/100 — total cost = −27 (per-dimension subtotals are capped at −15; an uncapped cost is shown in parentheses where the cap bites).

1.5.2 Ecosystem coupling Dimensions

Dimension Mechanism Description Present Cost
Performance R1 interpreted no AOT/JIT — 0
R2 GC pauses — 0
R3 JIT warmup — 0
Performance subtotal 0
Ecosystem Ec1 no package manager — 0
Ec2 fragmented tooling — 0
Ec3 small/niche/discontinued ✅ −8
Ec4 proprietary — 0
Ec5 platform-locked tooling — 0
Ec6 monoculture — 0
Ec7 legacy burden — 0
Ecosystem subtotal −8
Evolution V1 breaking changes — 0
V2 frozen — 0
V3 discontinued — 0
V4 glacial standards — 0
Evolution subtotal 0
Domain D1 domain/vendor lock-in ✅ −15
D2 poor domain fit — 0
D3 framework forces architecture — 0
Domain subtotal −15
Learning L1 steep ✅ −8
L2 large surface/multi-paradigm — 0
L3 sparse docs — 0
Learning subtotal −8
Syntax S1 verbose — 0
S2 inconsistent — 0
S3 punctuation-heavy — 0
Syntax subtotal 0
Testing G1 weak tooling — 0
G2 poor debugging — 0
G3 runtime-only errors — 0
Testing subtotal 0
Security Q1 memory-unsafe — 0
Q2 dynamic/weak typing risk — 0
Q3 known vulnerability/injection — 0
Security subtotal 0

Meta Dimensions score: 69/100 — total cost = −31 (per-dimension subtotals are capped at −15; an uncapped cost is shown in parentheses where the cap bites).

1.5.3 Engineering readiness Dimensions

Dimension Mechanism Description Present Cost
Reproducibility Y1 build not reproducible ✅ −8
Y2 dependencies not pinned ✅ −8
Reproducibility subtotal −15 (−16)
Supply chain Y3 no signed provenance ✅ −8
Y4 registry without namespacing ✅ −4
Supply chain subtotal −12
Observability Y5 no stable tracing standard ✅ −8
Y6 no structured logging ✅ −4
Observability subtotal −12
Feedback Y7 slow build — 0
Y8 no fast in-editor analysis — 0
Feedback subtotal 0
Interop Y9 no foreign-function interface — 0
Y10 no portable target ✅ −4
Interop subtotal −4
Governance Y11 single-vendor governance ✅ −8
Y12 closed specification ✅ −8
Governance subtotal −15 (−16)

Readiness Dimensions score: 42/100 — total cost = −58 (per-dimension subtotals are capped at −15; an uncapped cost is shown in parentheses where the cap bites).

Verdict: SPARK’s design yields low core coupling for the work it is built for, and its platform cost is the price of a narrow domain. The static type system is Ada’s, the contracts and flow aspects make every global dependency explicit, an ownership policy removes coupling through shared references, and the toolchain proves the run-time checks that other languages leave to a test suite. The only scored core loss is P1: the language is a subset of Ada and does not exist apart from that platform. Main strengths: GNATprove, a toolchain qualified for DO-178C, DO-333 credit for the proof, and industrial use at Airbus, Thales, and Lockheed Martin; main weaknesses: an ecosystem that is a subset of Ada’s, a domain lock-in to high-assurance systems, and one of the steepest learning curves here.

The formal development. The definitions, theorems, and proofs behind this page are published in:

All published papers

References

[1]
Y. Loth, “On the nature of coupling: All coupling as shared resource access.” Zenodo, Aug. 2026. doi: 10.5281/zenodo.21925122.
[2]
Y. Loth, “Coupling as a consequence of cohesion: Decomposition, the coupling floor, and domain-imposed coupling.” Zenodo, Aug. 2026. doi: 10.5281/zenodo.21925201.
[3]
Y. Loth, “On the nature of cohesion: Cohesion as correctness relative to a partitioning rule.” Zenodo, Jul. 2026. doi: 10.5281/zenodo.21703193.
[4]
AdaCore and ALTRAIN, “SPARK user’s guide.” AdaCore, 2024. Available: https://docs.adacore.com/spark2014-docs/html/ug/
[5]
R. Pereira et al., “Energy efficiency across programming languages: How do energy, time, and memory relate?” in Proceedings of the 10th ACM SIGPLAN international conference on software language engineering (SLE), 2017, pp. 256–267. doi: 10.1145/3136014.3136031.
[6]
R. Pereira et al., “Ranking programming languages by energy efficiency,” Science of Computer Programming, 2021, doi: 10.1016/j.scico.2021.102609.
[7]
N. van Kempen, H.-J. Kwon, D. T. Nguyen, and E. D. Berger, “It’s not easy being green: On the energy efficiency of programming languages,” in Proceedings of the 40th IEEE/ACM international conference on automated software engineering (ASE), 2025. doi: 10.1109/ASE63991.2025.00131.
[8]
S. Joel, J. J. Wu, and F. H. Fard, “A survey on LLM-based code generation for low-resource and domain-specific programming languages,” ACM Transactions on Software Engineering and Methodology, 2025, doi: 10.1145/3770084.