Comment by 0dyl

My 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 https://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).