News for hackers. Stuff that matters.
Re:FOSDEM 2025: The state of Rust trying to catch up with Ad... by ajdude on Monday February 10, 2025 @07:03AM (#42999326)
With Ada/SPARK (and hopefully Rust) this can be checked at compile time to formally prove code. You can also catch the runtime exceptions and handle them accordingly if you're not using SPARK.

The presentation right before the Rust one[1] actually did a bit of a dive into this.

I recently created a UUID library in Ada, and I'm able to validate an input string on the datatype level without ever having to worry about doing so in the function itself:

   subtype UUID_String is String (1 .. 36)
      with Dynamic_Predicate =>
         (for all I in UUID_String'First .. UUID_String'Last =>
            (case I is
               when 9 | 14 | 19 | 24 => (UUID_String (I) = '-'),
               when others =>
                  (UUID_String (I) in '0' .. '9' | 'A' .. 'F' | 'a' .. 'f')));
Now my function simply needs to be:

   function From_String (From : UUID_String) return UUID
      with Pre => From in UUID_String;
And I can code the function with the confidence that it won't be processing a malformed string.

[1] I don't think the video is ready yet, but you can view the slides here: https://fosdem.org/2025/events/attachments/fosdem-2025-4879-...

There are no comments on this comment yet.