Our great sponsors
-
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
> Consider a program in which an array was accessed based on the index provided by some user input -- how could this ever be proven to never go out of bounds?
It's a type constraint on the index. In most programming languages we're used to the index value is some machine type, like a 32-bit unsigned integer, but that's arbitrary, the language can say OK, this is an index into an array of sixteen things, so, the index must be between 0 and 15 inclusive.
Now, depending on the software you might just have to write bounds checks yourself to satisfy this constraint, so you just made more work for yourself, but if your software actually deals in types that can and perhaps should be constrained properly elsewhere this approach means you get a compiler error not a runtime failure.
Suppose we've got code that does foo[k] where foo is an array of eight things and k is an unsigned variable with the bottom four bits of a value from an image file that's supposed to be the CGA medium resolution colour palette ID (0, 1, or 2). Alas the file might be corrupt or malicious and those bottom bits could be, for example 10.
In C and C++ foo[k] compiles, and when the corrupt file is used there is Undefined Behaviour
In Rust foo[k] compiles, and when the corrupt file is used the program panics on this line
In WUFFS foo[k] doesn't compile, variable k is the wrong type for indexing foo.
https://github.com/google/wuffs/blob/main/doc/wuffs-the-lang...
Now, WUFFS is not a general purpose programming language. You should not write an operating system, a web server, a compiler in WUFFS. But, you should write your thumbnail making routine, your PDF validation code, your audio compressor in WUFFS, because in choosing not to be a general purpose language WUFFS is freed to simply always be safe. That WUFFS thumbnail code might make the RCE attempt from Leet Hacker into a blue rectangle, or crop all the executives photos to just their nose, but it simply cannot accidentally create a reverse shell, or spew passwords into the thumbnails, or a billion other things which Rust would make difficult to do by mistake but never impossible.
> I don't understand the "spiritual successor" part: Go intentionally broke ABI compatibility with the C world and intentionally does a lot of very un-C-like things: a large standard library, a GC'd runtime, a compiler toolchain that reimplements the "standard" toolchain, etc.
Could you explain "broke ABI compatibility with [...] C"? Do you mean broke compatibility with platforms' de facto C ABIs?
"Go bears a surface similarity to C and, like C, is a tool for professional programmers, achieving maximum effect with minimum means. But it is much more than an updated version of C."
- Preface of "The Go Programming Language"[1][2]
[1]: https://www.gopl.io
[2]: https://www.gopl.io/ch1.pdf
> how could this ever be proven to never go out of bounds?
I've done this in Ada/SPARK.
My simple_regex implementation of Rob Pike's algorithm (https://github.com/pyjarrett/simple_regex) based on this blog post (https://benhoyt.com/writings/rob-pike-regex/), is proved not to crash on overflow or bounds checks.
for CI have you tried to use buildkit persistent runners with caching + https://github.com/LukeMathWalker/cargo-chef ?