Ada's dependent types, and its types as a whole
Ada’s type system and memory model are highlighted as powerful but underused alternatives to mainstream “safe” languages like Rust and C++. Commenters delve into features such as ranged and discriminated types, subtype predicates, a secondary stack for dynamic data, and the SPARK toolset for formal verification, contrasting them with full dependent type theory and Rust’s borrow checker. Adoption challenges—including verbose syntax, historical licensing and tooling issues, weaker library and package ecosystems, and limited industry demand outside safety‑critical and embedded systems—are seen as key reasons Ada remains niche despite its strengths.
Memory model and “two stacks”
- Ada implementations commonly use a secondary stack for dynamically sized data, separate from the call stack.
- This solves many “short-lived allocation” problems that arenas/scratch buffers address in C/C++ and games.
- Language-level support lets the compiler statically track secondary-stack usage, free earlier, and maintain safety; manual arenas can’t reclaim mid-stack allocations without resetting everything.
- Some note that similar behavior could be done with the main stack and copying, but the dedicated second stack is simpler and ABI-friendly.
Ada vs. Rust and other languages
- Several commenters argue Ada is underrated compared to Rust, especially for embedded/MCU firmware that avoids dynamic allocation.
- They stress Ada’s strengths: ranged types, representation clauses for bitfields and serialisation, decimal types, strong spec/reference manual, and SPARK for formal verification.
- Rust is praised for memory safety and ecosystem (Cargo, libraries) and for attracting new kernel contributors, but criticized for focusing mostly on memory safety rather than functional correctness.
- Some wish Linux had Ada-based drivers, citing SPARK and representation clauses; others doubt maintainers would accept it.
Dependent types and SPARK
- Multiple posts challenge the article’s framing of Ada as “dependently typed” in the type-theory sense.
- Classic dependent types (as in Coq/Agda/Lean) allow expressing and proving properties like “sorting always returns a sorted list” at the type level.
- Ada’s subtype predicates and discriminated records are powerful and can encode runtime-checked invariants; static predicates exist but are limited.
- SPARK adds a separate verification layer: Ada code plus contracts is translated to Why3/SMT provers; examples include fully proved sorting.
- Consensus: Ada/SPARK gives strong, practical verification, but is not a full Martin-Löf–style dependently typed language.
Tooling, ecosystem, and licensing
- Complaints: historically expensive/proprietary compilers, confusing licensing, and weaker general-purpose libraries (e.g., TLS/crypto, codecs, Android NDK story).
- Responses: GNAT (Ada in GCC) is FOSS; multiple commercial vendors exist; Alire and the “getada” installer now make setup easy on major platforms.
- Some worry about GPLv3 implications; others counter that compiler/runtime licenses don’t infect user code.
- Lack of a rich, modern standard ecosystem is seen as a major barrier compared to languages like Rust, Go, Python.
Syntax, readability, and IDE support
- Ada’s verbose, English-like syntax and
end Name;blocks are seen by some as hard to skim compared to brace-heavy C/Rust. - Others find Ada’s explicit structure easier to read and less ambiguous, especially in large, nested code, and note that end-names are optional.
- Several argue modern editors (block selection, sticky scroll, jumping to matching delimiters) mitigate most syntax readability issues regardless of language.
Adoption, domains, and jobs
- Historically strong in defense, aerospace, high-integrity embedded systems; also influenced VHDL and PL/SQL/pgSQL.
- Reported non-military uses include warehouse management software. Some suggest more jobs now exist in VHDL than in Ada itself.
- Ada’s adoption was hurt by early compiler pricing, lack of free tools during key growth periods, and today by fashion/mindshare favoring Rust and C-like syntaxes.
Trying Ada
- Recommended entry points: FOSS GNAT via package managers, Alire as a package manager/toolchain orchestrator, the “getada” curl-based installer, and browser-based tutorials and playgrounds.