Ada's dependent types, and its types as a whole

Original Article ↗ Hacker News Discussion ↗

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.