A Comparison of Ada and Rust, Using Solutions to the Advent of Code

18 year old me couldn't appreciate how beautiful a language it is but in my 40s I finally do.

I distinctly remember arguments for functions working on array of 10. Oh, you want array of 12? Copy-paste the function to make it array of 12. What a load of BS.

It took Pascal years to drop that constraint, but by then C had already won.

I never ever wanted the compiler or runtime to check a subrange of ints. Ever. Overflow as program crash would be better, which I do find useful, but arbitrary ranges chosen by programmer? No thanks. To make matters worse, those are checked even by intermediate results.

I realize this is opinioned only on my experience, so I would appreciate a counter example where it is a benefit (and yes, I worked on production code written in Pascal, French variant even, and migrating it to C was hilariously more readable and maintainable).

[0] https://news.ycombinator.com/item?id=45474777

There were some talks about general pattern type, but it's not even approved as an experiment, not to talk about RFC or stabilization.

There is the wisdom that it is impossible to deliver C++ without pervasive safety issues, for which there are many examples, and on the other hand there are people delivering C++ in high-assurance environments with extremely low defect rates without heroic efforts. Many stories can be written in that gap. C++ can verify many things that are not verifiable in Rust, even though almost no one does.

It mostly isn’t worth the argument. For me, C++20 reached the threshold where it is practical to design code where large parts can be formally verified in multiple ways. That’s great, this has proven to be robust in practice. At the same time, there is an almost complete absence of such practice in the C++ literature and zeitgeist. These things aren’t that complex, the language users are in some sense failing the language.

The ability to codegen situationally specific numeric types is just scratching the surface. You can verify far weirder situational properties than numeric bounds if you want to. I’m always surprised by how few people do.

I used to be a C++ hater. Modern C++ brought me back almost purely because it allows rich compile-time verification of correctness. C++11 was limited but C++20 is like a different world.

  let ageFails = (200 + 2).Age
  Error: 202 can't be converted to Age

  import std/strutils

  stdout.write("What's your age: ")
  let age = stdin.readLine().parseInt().Age

  $ nim r main.nim
  What's your age: 999
  Error: unhandled exception: value out of range: 999 notin 0 .. 200 [RangeDefect]

Modifying a compiler to emit a message at every point that a runtime check is auto-inserted should be pretty simple. If this was really that much of an issue it would have been addressed by now.

Ada's compile time verification is very good. With SPARK it's even better.

Runtime constraints are removable via Pragma so there's no tradeoff at all with having it in the language. One Pragma turns them into static analysis annotations that have no runtime consequences.

If it fails at run time, it could be the reason you get paged at 1am because everything's broken.

It's a good example for the "Parse, don't validate" article (https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...). Instead of creating a function that accepts `int` and returns `int` or throws an exception, create a new type that enforces "`int` less than equal 200"

  class LEQ200 { ... }
  LEQ200 validate(int age) throws Exception {
      if (age <= 200) return age;
      else throw Exception();
  }

  LEQ200 works = validate(200);
  // LEQ200 fails = validate(201);
  // LEQ200 hmmm = works + 1; // Error in Java
  LEQ hmmm = works.add(1); // Throws an exception or use Haskell's Either-type / Rust's Result-type

These kind of compile-time type voodoo requires a different mindset compared to cargo-cult Java OOP. Whether something like this is ergonomic or performance-friendly depends on the language's support itself.

https://learn.adacore.com/courses/intro-to-ada/chapters/cont...

You may choose to think from safety guarantee hierarchy perspective like (Bottom = foundation... Top = highest assurance)

Layer 6: FORMAL PROOFS (functional correctness, no RT errors) Ada/SPARK: built-in (GNATprove) Rust: external tools (Kani, Prusti, Verus)

Layer 5: TIMING / REAL-TIME ANALYSIS (WCET, priority bounds) Ada: Ravenscar profile + scheduling analysis Rust: frameworks (RTIC, Embassy)

Layer 4: CONCURRENCY DETERMINISM (predictable schedules) Ada: protected objects + task priorities Rust: data-race freedom; determinism via design

Layer 3: LOGICAL CONTRACTS & INVARIANTS (pre/post, ranges) Ada: Pre/Post aspects, type predicates (built-in) Rust: type states, assertions, external DbC tools

Layer 2: TYPE SAFETY (prevent invalid states) Ada: range subtypes, discriminants Rust: newtypes, enums, const generics

Layer 1: MEMORY SAFETY & DATA-RACE FREEDOM Ada: runtime checks; SPARK proves statically Rust: compile-time via ownership + Send/Sync

    with Ada.Text_IO; use Ada.Text_IO;

    procedure Restricted_Number_Demo is

        -- Define a restricted subtype of Integer
        subtype Small_Positive is Integer range 1 .. 100;

        -- Define a restricted subtype of Float
        subtype Probability is Float range 0.0 .. 1.0;

        -- Variables of these restricted types
        X : Small_Positive := 42;
        P : Probability    := 0.75;

    begin
        Put_Line("X = " & Integer'Image(X));
        Put_Line("P = " & Float'Image(P));

        -- Uncommenting the following line would raise a Constraint_Error at runtime
        -- X := 200;

    end Restricted_Number_Demo;

Now I've set (and possibly moved) the goalposts, I can prove my point: C# already does this! You can use async across multiple threads and cancellation happens with cancellation tokens that are thread safe. Having a version where interruptable calls are blocking rather than async (in the language sense) would actually be easier to implement (using the same async-capable APIs under the hood e.g., IOCP on Windows).

Dropping a future does not cancel a concurrently running (tokio::spawn) task. It will also not magically stop an asynchronous I/o call, it just won't block/switch from your code anymore while that continues to execute. If you have created a future but not hit .await or tokio::spawn or any of the futures:: queue handlers, then it also won't cancel it it just won't begin it.

Cancellation of a running task from outside that task actually does require explicit cancelling calls IIRC.

Edit here try this https://cybernetist.com/2024/04/19/rust-tokio-task-cancellat...

In her presentation on async cancellation in Rust, she spoke pretty extensively on cancel safety and correctness, and I would recommend giving it a watch or read.

https://sunshowers.io/posts/cancelling-async-rust/

[0] https://en.wikipedia.org/wiki/Scheduler_activations, https://dl.acm.org/doi/10.1145/121132.121151 | Akin to thread-per-core

[1] Stackless coroutines and event-driven programming

[2] User-level virtual/green threads today, plus responsiveness to blocking I/O events

Specs for other languages are also for a specific version/snapshot.

It's also a specific version of a compiler that gets certified, not a compiler in perpetuity, no matter what language.

(Already mentioned) CakeML would be another example, together maybe with its Pancake sibling.

Also: WebAssembly!

Another, https://cakeml.org/

[1]: https://en.wikipedia.org/wiki/ATS_(programming_language)