3 ms·

We could do that in Turbo Pascal, 35 years ago. To be honest, it wasn't particularly useful, because it requires runtime checks which panic if they fail. What

We could do that in Turbo Pascal, 35 years ago. To be honest, it wasn't particularly useful, because it requires runtime checks which panic if they fail. What is their practical use in the modern age?

ajdude 2y ago
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-...
tialaramex 2y ago
In Rust the bit patterns which are not occupied by a value are free for some other use, Rust calls this a "niche" and uses it extensively in its sum types. This lets us have all the performance advantages of using magic sentinel values occupying those bit pattern, but with the same ergonomics as for an ordinary sum type. For example in C a Unix file descriptor is just an integer. 0, 100, 1000 - all perfectly reasonable file descriptors. But, -1 is not a valid file descriptor, so Rust's OwnedFd is internally just an ordinary C-style integer, except, it's never -1 as a result Rust's Option<OwnedFd> is the same size as the C integer, you'll get the same machine code as the C integer, but in C you need to remember to check it's not -1 before using it, in Rust you won't make that mistake because that's not Some(fd) that's None. Rust does this with its references, Option<&T> is the same size as &T, depending on what exactly T is that's probably "really" a machine address in a CPU register, and so None is the same CPU register with an all-zeroes bit representation. My favourite non-standard library use of this feature is CompactString. CompactString is the SSO (Small String Optimisation) made famous in C++ but applied to Rust's strings. Rust's native String type is as simple as possible, thus no SSO, it's actually internally Vec<u8> plus rules to ensure it is always UTF-8 encoded text. SSO in C++ standard libraries means that "Dog" or "Cheese" are stored inline in the type itself, no need for a heap allocation. CompactString takes that to an extreme. While a typical C++ std::string might allow you to store "ycombinator.com" inside the 32 byte data structure, CompactString fits "https://ycombinator.com/ https://ycombinator.com/" in its just 24 bytes! It does this by being able to distinguish whether that last byte is a valid final UTF-8 code unit, if it is then this is a 24 byte string, but if it's not then it signals how long the rest of the string is and how the other 23 bytes should be interpreted.
- kccqzy 2y ago
  Minor correction about C++ SSO: different C++ implementations have different small string capacities. In clang and libc++, you can store 22 bytes of short string when the data structure itself is 24 bytes. This is more than what MSVC or gcc can do. https://devblogs.microsoft.com/oldnewthing/20240510-00/?p=109742 https://devblogs.microsoft.com/oldnewthing/20240510-00/?p=10...
pjmlp 2y ago
Just like bounds checking in Rust. Some type safety conditions can naturally only be checked at run-time. And actually, checks are done at compile time if the compiler is able to see what is being used on the spot.
- tialaramex 2y ago
  Also, sometimes you can arrange that the "check" is just the natural way to express what you meant in the language, so whether it's a runtime check or not, the ergonomics are improved enormously, it feels natural. In Rust NonZeroI8::new(n).unwrap() is either a NonZeroI8 or, if n was zero, it panics because we asked to unwrap the Option and that's None. What's inside NonZeroI8::new ? Literally a cast. When compiled this is nothing at all, no machine code is generated. It is relying on the fact that Option<NonZeroI8> has bit pattern 00000000 for None, and that's also the bit pattern for the integer zero. So if we ask at compile time, NonZeroI8::new(FOO).unwrap() for some constant FOO, the compiler will, at compile time, transform the FOO bit pattern, if it's all zeroes this code is just a runtime panic, and if it's on the clear through line (e.g. the only code in the main function) by default the compiler says well that's not going to work, here's a compiler error [if you actually want a program which just panics when run you can ask for that with a compiler setting, good luck to you]. If FOO isn't zero then, still at compile time, now we've got a NonZeroI8 with value FOO
naasking 2y ago
> To be honest, it wasn't particularly useful, because it requires runtime checks which panic if they fail. Checking at runtime is 100% still incredibly useful. That's how you enforce critical program invariants to avoid security vulnerabilities or prevent invalid states that could ruin the program's data.
etrez 2y ago
* Splitting large enumerated types into smaller ones * Using the same range for arrays indexes, "for" loops parameters which index those arrays. In those cases a good compiler removes the useless run-time checks! Ada range types can have bounds that are known only at run-time. It was not possible with Pascal. To see subtypes in action: another FOSDEM presentation: https://fosdem.org/2025/schedule/event/fosdem-2025-5148-advent-of-compression-writing-a-working-bzip2-encoder-in-ada-from-scratch-in-a-few-days/ https://fosdem.org/2025/schedule/event/fosdem-2025-5148-adve...

ajdude 2y ago

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

tialaramex 2y ago

In Rust the bit patterns which are not occupied by a value are free for some other use, Rust calls this a "niche" and uses it extensively in its sum types. This lets us have all the performance advantages of using magic sentinel values occupying those bit pattern, but with the same ergonomics as for an ordinary sum type. For example in C a Unix file descriptor is just an integer. 0, 100, 1000 - all perfectly reasonable file descriptors. But, -1 is not a valid file descriptor, so Rust's OwnedFd is internally just an ordinary C-style integer, except, it's never -1 as a result Rust's Option<OwnedFd> is the same size as the C integer, you'll get the same machine code as the C integer, but in C you need to remember to check it's not -1 before using it, in Rust you won't make that mistake because that's not Some(fd) that's None. Rust does this with its references, Option<&T> is the same size as &T, depending on what exactly T is that's probably "really" a machine address in a CPU register, and so None is the same CPU register with an all-zeroes bit representation. My favourite non-standard library use of this feature is CompactString. CompactString is the SSO (Small String Optimisation) made famous in C++ but applied to Rust's strings. Rust's native String type is as simple as possible, thus no SSO, it's actually internally Vec<u8> plus rules to ensure it is always UTF-8 encoded text. SSO in C++ standard libraries means that "Dog" or "Cheese" are stored inline in the type itself, no need for a heap allocation. CompactString takes that to an extreme. While a typical C++ std::string might allow you to store "ycombinator.com" inside the 32 byte data structure, CompactString fits "https://ycombinator.com/ https://ycombinator.com/" in its just 24 bytes! It does this by being able to distinguish whether that last byte is a valid final UTF-8 code unit, if it is then this is a 24 byte string, but if it's not then it signals how long the rest of the string is and how the other 23 bytes should be interpreted.

kccqzy 2y ago
Minor correction about C++ SSO: different C++ implementations have different small string capacities. In clang and libc++, you can store 22 bytes of short string when the data structure itself is 24 bytes. This is more than what MSVC or gcc can do. https://devblogs.microsoft.com/oldnewthing/20240510-00/?p=109742 https://devblogs.microsoft.com/oldnewthing/20240510-00/?p=10...

pjmlp 2y ago

Just like bounds checking in Rust. Some type safety conditions can naturally only be checked at run-time. And actually, checks are done at compile time if the compiler is able to see what is being used on the spot.

tialaramex 2y ago
Also, sometimes you can arrange that the "check" is just the natural way to express what you meant in the language, so whether it's a runtime check or not, the ergonomics are improved enormously, it feels natural. In Rust NonZeroI8::new(n).unwrap() is either a NonZeroI8 or, if n was zero, it panics because we asked to unwrap the Option and that's None. What's inside NonZeroI8::new ? Literally a cast. When compiled this is nothing at all, no machine code is generated. It is relying on the fact that Option<NonZeroI8> has bit pattern 00000000 for None, and that's also the bit pattern for the integer zero. So if we ask at compile time, NonZeroI8::new(FOO).unwrap() for some constant FOO, the compiler will, at compile time, transform the FOO bit pattern, if it's all zeroes this code is just a runtime panic, and if it's on the clear through line (e.g. the only code in the main function) by default the compiler says well that's not going to work, here's a compiler error [if you actually want a program which just panics when run you can ask for that with a compiler setting, good luck to you]. If FOO isn't zero then, still at compile time, now we've got a NonZeroI8 with value FOO

naasking 2y ago

> To be honest, it wasn't particularly useful, because it requires runtime checks which panic if they fail. Checking at runtime is 100% still incredibly useful. That's how you enforce critical program invariants to avoid security vulnerabilities or prevent invalid states that could ruin the program's data.

etrez 2y ago

* Splitting large enumerated types into smaller ones * Using the same range for arrays indexes, "for" loops parameters which index those arrays. In those cases a good compiler removes the useless run-time checks! Ada range types can have bounds that are known only at run-time. It was not possible with Pascal. To see subtypes in action: another FOSDEM presentation: https://fosdem.org/2025/schedule/event/fosdem-2025-5148-advent-of-compression-writing-a-working-bzip2-encoder-in-ada-from-scratch-in-a-few-days/ https://fosdem.org/2025/schedule/event/fosdem-2025-5148-adve...