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 accor

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-understanding-liquid-types-contracts-and-formal-verification-with-ada-spark/slides/237311/liquid-ty_dasDD3B.pdf https://fosdem.org/2025/events/attachments/fosdem-2025-4879-...