Ada Quest is an interactive on-ramp for learning Ada and SPARK through small systems bugs, compiler-style feedback, and proof-oriented missions.
The project exists to make Ada feel alive in the first ten minutes: useful, readable, safe by construction, and worth exploring beyond nostalgia.
- A static browser app with no install step
- Four Ada/SPARK missions:
- packet bounds with constrained subtypes and preconditions
- unit-safe APIs with distinct numeric types
- shared state with protected types
- SPARK contracts for a bounded stack
- A simple in-browser editor
- Simulated compiler/proof checks for each mission
- Starter-kit cards for future Alire and
adaquestCLI flows - A launch/campaign board for contributors who want to grow the project
The current MVP simulates compiler and proof feedback in the browser. That is intentional for the first public seed.
The next major milestone is a real Ada runner that can compile mission code with GNAT and, where appropriate, run GNATprove for SPARK checks.
For more context, see docs/gnat-gnatprove.md.
Open index.html directly, or serve the folder locally:
python3 -m http.server 8765 --bind 127.0.0.1Then visit:
http://127.0.0.1:8765/index.html
node scripts/validate-missions.jsor:
npm testThe validation script loads the app mission data and checks that every included solution passes the current simulated mission checks.
Good first contributions include:
- Add a beginner Ada mission
- Improve mission wording for Ada newcomers
- Add syntax highlighting
- Convert mission data into JSON
- Add shareable mission URLs
- Create real Alire starter templates
- Prototype a GNAT compile runner
- Prototype a GNATprove runner
See CONTRIBUTING.md, ROADMAP.md, docs/mission-format.md, and docs/gnat-gnatprove.md.
Ada Quest is not trying to win a language war.
The message is:
Ada is for software that has to keep its promises.
If Rust made people care about memory safety, Ada and SPARK can help people care about contracts, ranges, concurrency, proof, and whole-system intent.
MIT. See LICENSE.