Rust’s built-in notion of safety is intentionally focused on memory + data-race properties at compile time. logic, timing, and determinism are left to libraries and design. Ada (with SPARK & Ravenscar) treats contracts, concurrency discipline, and timing analysis as first-class language/profile concerns hence a broader safety envelope.

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

As the OP mentioned, restricted number ranges:

    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;

Ideally, a compiler can statically prove that values stay within the range; it's no different than proving that values of an enumeration type are valid. The only places where a check is needed are conversions from other types, which are explicit and traceable.

This is basically excuses being made by C people for use of a language that wasn't designed for and isn't suitable for safety critical software. "We didn't even need that feature!"

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.

I like how better more reliable code is more expensive to certify and the problem is the code and not the certification criteria/process being flawed.

> as it inserts run-time checks that are not easily traceable to source code

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.

To elaborate on siblings compile time vs run time answer: if it fails at compile time you'll know it's a problem, and then have the choice to not enforce that check there.

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

Like other sibling replies said, subranges (or more generally "Refinement types") are more about compile-time guarantees. Your example provides a good example of a potential footgun: a post-validation operation might unknowingly violate an invariant.

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.

It’s a question of compile time versus runtime.

Yeah it’s something that code would compile down to. You can skip Java and write assembly directly, too.

Your example also gets evaluated at comptime. For more complex cases I wouldn't be able to tell you, I'm not the compiler :) For example, this get's checked:

  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]

If you're using SPARK, it'll catch at compile time if there's ever a possibility that it would fit within that condition. Otherwise it'll throw an exception (constraint_error) during runtime for you to catch.

No, range types are at best a very limited piece of DbC. Design by Contract lets you state much more interesting things about your program. It's also available in Ada, though.

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

A whole zoo of dimensional analysis in programming languages : https://www.gmpreussner.com/research/dimensional-analysis-in...

Nice, didn't know that. I keep seeing praise for F# so I should finally take a look.

This is an unfortunate reality. C++ has evolved into a language capable of a surprisingly deep compile-time verification but almost no one uses that capability. It reflects somewhat negatively on the C++ developer community that problems easily solved within the language are routinely not solved, though the obsession with backward compatibility with old versions of the language plays a role. If you fully leverage it, I would argue that recent versions of C++ are actually the safest systems language. Nonetheless, almost no one has seen code bases that leverage that verification capability to its maximum. Most people have no clue what it is capable of.

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.

AFAIK the current status is that it's internal to std (used to implement `NonNull` and friends) and not planned to be exposed.

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

I would guess that Ada is simply more known. Keep in mind that tech exploded in the past ~3.5 decades whereas those languages are much older and lost the popularity contest. If you ask most people about older languages, the replies other than the obvious C and (kind of wrong but well) C++ are getting thin really quickly. COBOL, Ada, Fortran, and Lisp are probably what people are aware of the most, but other than that?

For me it's because I learned Ada in college.

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

Turbo Pascal could check ranges on assignment with the {$R+} directive, and Delphi could check arithmetic overflow with {$Q+}. Of course, nobody wanted to waste the cycles to turn those on :)

I would argue that was one of the reasons why those languages lost.

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).

As a sibling comment[0] mentioned, pattern types are actively being worked on.

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