TRtremon·Nov 1, 2025
That links gives me a 404. Does it require membership of some organization before you're allowed to view it?
edit: did you mean https://github.com/AdaCore/spark2014 ?
In Open-Source Ada: From Gateware to ApplicationAdaCore
spark2014
Ada2017–2025
AdaCore / spark2014
spark2014
SPARK 2014 is the new version of SPARK, a software development technology specifically designed for engineering high-reliability applications.
11Distinct people
14Mentions
1Explicit recommenders
332GitHub stars
What to know before exploring
What it is
SPARK 2014 is the new version of SPARK, a software development technology specifically designed for engineering high-reliability applications.
GitHub
Where it is used
No documented product use was verified in the last source check.
What people are saying
So it has typestates. (I recommend anyone [0] and its HN thread [1] for detail.) I think that's a great language feature for helping to avoid bugs, especially the kind that…
MaxBarraclough used a recommendation phrase. One indexed comment matches. This is a phrase match, not a verdict.
No classified warning is attached to this page. Read the discussions before treating silence as approval.
Also in these discussions
No other repository is repeatedly linked in the same discussions.
This week on Hacker News
Nov 8–Nov 15 UTC · Direct repository links and separately labeled related project stories. Indexed through 11/15/2026, 7:24:48 PM UTC.
No direct repository links were found in the indexed HN discussions over the past seven days. Older discussions are available below.
Mentions over time
HN mentions by year14 dated mentions
Observed mentions: 2017-08-24 14:15:43 UTC to 2025-11-01 20:13:44 UTC.
Counts come from the repository’s dated source evidence. Index cutoff: 2026-11-02 08:16:59 UTC.
View mention counts and date ranges
| Period | Start (UTC) | End (exclusive, UTC) | Mentions | Submissions | Comments |
|---|---|---|---|---|---|
| 2017 | 2017-01-01 00:00:00 UTC | 2018-01-01 00:00:00 UTC | 1 | 0 | 1 |
| 2018 | 2018-01-01 00:00:00 UTC | 2019-01-01 00:00:00 UTC | 0 | 0 | 0 |
| 2019 | 2019-01-01 00:00:00 UTC | 2020-01-01 00:00:00 UTC | 2 | 0 | 2 |
| 2020 | 2020-01-01 00:00:00 UTC | 2021-01-01 00:00:00 UTC | 3 | 0 | 3 |
| 2021 | 2021-01-01 00:00:00 UTC | 2022-01-01 00:00:00 UTC | 0 | 0 | 0 |
| 2022 | 2022-01-01 00:00:00 UTC | 2023-01-01 00:00:00 UTC | 0 | 0 | 0 |
| 2023 | 2023-01-01 00:00:00 UTC | 2024-01-01 00:00:00 UTC | 0 | 0 | 0 |
| 2024 | 2024-01-01 00:00:00 UTC | 2025-01-01 00:00:00 UTC | 1 | 0 | 1 |
| 2025 | 2025-01-01 00:00:00 UTC | 2026-01-01 00:00:00 UTC | 7 | 0 | 7 |
What Hacker News says
7 sourcesSPARK tools are also open source. The main tool `gnatprove` is based on GCC as well. https://github.com/AdaCore/spark2014
It's not a community project, AFAICT. Few people know how to build it from source.
In Open-Source Ada: From Gateware to ApplicationMy apologies for getting frustrated. I shouldn’t have done that.
This is bit on info-dump. I’m not the best at expressing myself and so some parts may not be clear. Please feel free to ask for clarification or any further questions.
Pattern matching is available as a language extension (currently) exclusive to GNAT GCC. It’s not in the reference manual, which means it’s not part of standardised Ada (yet). It’s intended to be an experiment or prototype for what will eventually become a standardised language feature (the standardised feature may be different, or it could be rejected, as the standardisation committee is composed of multiple compiler vendors).
As is, that pattern matching feature works in both normal Ada and in SPARK mode on GNAT GCC 15.2. The flag to enable it is “-gnatX0”. Please see these: https://godbolt.org/z/d55ddznfn
h
Read the rest
ttps://gcc.gnu.org/onlinedocs/gnat_rm/Case-pattern-matching...
https://gcc.gnu.org/onlinedocs/gcc-15.1.0/gnat_rm/How-to-act...
In the Godbolt example, that is in normal Ada.
You are not alone in finding the Ada community difficult to navigate. The “ada-spark-rfcs” repository you linked is a community outreach program of AdaCore to solicit feedback from programmers in venues they’re more likely to use. Those RFCs are then forwarded to the Ada Rapporteurs Group (ARG) who focus on the development of standardised Ada. Their issues, mailing list and meeting minutes can be found at: http://www.ada-auth.org/arg.html
SPARK doesn’t add features to Ada; instead, it’s a subset of features that can be easily proven by SMTs for formal verification. The special things in SPARK (extra attributes and pragmas, which Ada implementations are allowed to define) are only to aid formal verification. When language features are added, they’re added to Ada first and subsequently potentially enabled in SPARK.
I admit that calling it “ada-spark-rfcs” is kinda confusing - it’s just dumping ground for ideas for Ada and SPARK. For example, the multiple ghost levels RFC really only applies to SPARK, as ghost code only exists to improve verifiability. The final modifier RFC is for Ada proper, and it’ll probably apply to SPARK as it allows OOP.
The situation regarding compiler available is confusing and it made me nervous when I was first learning about the language.
GNAT GCC has two versions: FSF and PRO. The FSF (as in the Free Software Foundation) version is the publicly available version that’s in mainline GCC. PRO is for paying customers of AdaCore. From what I can tell, it’s built against an older version of the GCC backend. It tends to get those newest experimental features sooner, but they do trickle into FSF GCC. There have been points in time where I haven’t noticed any difference in feature set between GNAT PRO (according to the release notes) and those in FSF.
SPARK code works with both GNAT FSF and GNAT PRO. The formal verification tool for SPARK, GNATprove, is open source. https://github.com/AdaCore/spark2014
Have a great day. :)
Edit:
I’m not affiliated with AdaCore. I’ve never even spoken to one of their employees on the forums. I do use Ada, but only in my “side-business” (not making any money yet lol).
SPARK (Ada) is about as memory-safe as it gets.
https://github.com/AdaCore/spark2014
In Ask HN: Memory-safe low level languages?See also:
I can’t believe that I can prove that it can sort - https://news.ycombinator.com/item?id=31975507 - Jul 2022 (115 comments)
Here's some other sorting algorithms proven with SPARK, with much more straightforward proofs: https://github.com/AdaCore/spark2014/blob/master/testsuite/g...
In Is this the simplest (and most surprising) sorting algorithm ever? (2021)What are wavefronts? Not getting many search results on that, besides a few github issues mentioning them.
https://github.com/AdaCore/RecordFlux/issues/955
https://learn.adacore.com/search.html?q=wavefront&check_keyw... (nada)
https://docs.adacore.com/spark2014-docs/html/ug/search.html?... (nada)
https://github.com/AdaCore/spark2014/issues?q=wavefront%20 (nada)
In Nvidia Security Team: “What if we just stopped using C?” (2022)I really wish there was more active development on SPARK.
It's largely untouched over the last 10-years.
https://github.com/AdaCore/spark2014
For those not aware, SPARK gives even more safeguards/guarantees than Rust (see below) ... and also does it at compile time (when not all of Rust safeguards are at compile time).
https://blog.adacore.com/should-i-choose-ada-spark-or-rust-o...
In Nvidia Security Team: “What if we just stopped using C?” (2022)