|
|
Subscribe / Log in / New account

Undefined Behaviour as usual

Undefined Behaviour as usual

Posted Feb 25, 2024 2:54 UTC (Sun) by tialaramex (subscriber, #21167)
In reply to: Undefined Behaviour as usual by wtarreau
Parent article: Stenberg: DISPUTED, not REJECTED

> Sometimes you would just like to be able to tell the compiler "trust me, this variable is not null" or "trust me this value is always between 13 and 27" and be done with it.

These seem extremely dangerous and I would not recommend them. Being able to insist that things are true when maybe they aren't is almost certainly going to make the things you complain of even worse. Prefer instead to help the compiler figure out for itself that variables must have the properties you desire.

For example Rust's NonNull<T> is a pointer that's not null. If you have a pointer, you can ask NonNull::new to give you an Option<NonNull<T>> instead, and it will either give you Some(NonNull<T>) or None accordingly.

WUFFS will let you express "I claim that value is between 13 and 27" in code, and check that indeed it can see why value is between 13 and 27 so you're correct. For example:

assert value < 27 via "a < b: a < c; c <= b"(c: foo)

That says, a human has promised you elsewhere (in a list of propositions humans have proved) that this obvious rule about comparison operators is true. Using that proposition, and the facts that foo is less than or equal to 27 and that value is less than foo, you can see that value is less than 27. Done.

Note that this won't compile if you're wrong (e.g. value isn't less than foo) unless you fed WUFFS a faulty proposition and then relied on that proposition, so, don't do that, if you need to prove tricky things hire a mathematician. And especially note that I wrote _compile_ there. This isn't a runtime problem, WUFFS rejects faulty programs at compile time.


to post comments

Undefined Behaviour as usual

Posted Feb 25, 2024 10:35 UTC (Sun) by khim (subscriber, #9252) [Link] (1 responses)

> For example Rust's NonNull<T> is a pointer that's not null.

And yet you may use unsafe to forcibly shove null in it and then “bad thing happen”™.

You couldn't use your knowledge that NonNull<T> is just a 8byte piece of data in memory which accepts sequence of 64 zero bits just fine and use that to save some memory somewhere. This is just not guaranteed to work and people (and not the compiler!) would punish you if you would insist that it's just fine because you have unit tests and they are working.

That is the fundamental difference between C/C++ and Rust.

> Note that this won't compile if you're wrong (e.g. value isn't less than foo) unless you fed WUFFS a faulty proposition and then relied on that proposition, so, don't do that, if you need to prove tricky things hire a mathematician.

You have not have someone who kicks out the violators. Because every language is either safe, incomplete and non-self-hosting (and then you have some other language which is used to host that safe language) or unsafe, complete and, optionally, self-hosting.

And attempts to skip that duty of keeping violators in line just simply doesn't work: Java and PHP are memory safe languages, yet how many security breaches have people seen via programs written in these languages?

Compiler may help you to avoid stupid mistakes, but if you actively lie to the compiler then nothing may ever be truly reliable or secure.

Undefined Behaviour as usual

Posted Feb 26, 2024 2:47 UTC (Mon) by tialaramex (subscriber, #21167) [Link]

I would characterise what you've described as the fundamental difference as Safety Culture, and I agree it's the essential difference at the heart of Rust, more so than a technical difference like their very different answer to the question implied by Rice's Theorem (when we can't tell if this is a valid program, what then? Rust's answer is that this program does not compile, the C++ answer is that it must compile anyway)

For WUFFS it's not quite the same in two crucial ways, firstly because it's not a general purpose language it can't have and won't have a large audience. So it can be completely picky, it would be fine if they don't want people who like Vim, or anybody whose name has too many vowels in it, no problem.

Secondly though their safety is much more fundamental to the language itself. You could take Rust's technology and build something completely unsafe with that. The Rust community wouldn't, but it's not a restriction of the technology. WUFFS can't really do that, the technology doesn't really do anything else, there's a lot of clever maths stuff going on there which is heading for only one destination, certainty of correctness. The only other extraordinary thing about WUFFS is performance, but even there it does so in a way that only makes sense if you assume correctness is mandatory. I don't believe you would build this technology for any other reason.

For both reasons I don't think there's any need to "kick out the violators". To such people WUFFS makes no sense, it's like worrying about whether the crows on your web cam accept the Terms of Service of your ISP. The crows don't even understand what Terms of Service are as an idea, much less accept these particular terms.

In your terms I'd guess you'd consider WUFFS "incomplete". That's fine, it's not supposed to be "complete" in this sense.

Undefined Behaviour as usual

Posted Feb 25, 2024 11:19 UTC (Sun) by Wol (subscriber, #4433) [Link]

> > Sometimes you would just like to be able to tell the compiler "trust me, this variable is not null" or "trust me this value is always between 13 and 27" and be done with it.

> These seem extremely dangerous and I would not recommend them. Being able to insist that things are true when maybe they aren't is almost certainly going to make the things you complain of even worse. Prefer instead to help the compiler figure out for itself that variables must have the properties you desire.

Not quite the same thing, but again to be able to say "the only valid values are between 13 and 27". Then the compiler goes "if I detect a value that isn't, that's an error". Or trigger a warning "cannot prove boundaries are met".

Cheers,
Wol


Copyright © 2025, Eklektix, Inc.
Comments and public postings are copyrighted by their creators.
Linux is a registered trademark of Linus Torvalds