4 ms·

Maybe be less zealous and aware of your assumptions? Your assumption is that memory safety has to be baked in the language. It could be baked into proof assis

Maybe be less zealous and aware of your assumptions? Your assumption is that memory safety has to be baked in the language. It could be baked into proof assistants that are part of (optional or add-on) tooling, like what sel4 does. A simpler language makes this more possible, and the things that a proof assistants can do go far beyond what rust is able to provide, without sacrificing compilation speed or other forms of optimality (e.g. avoiding the heap) when you don't want or need such a high level of security guarantee (e.g. writing a cli tool that never sees the internet) As for me, I'm terrified that rusts complex macro system will hide/obfuscate discovery of other forms of security regression, like timing or energy side channels.

staticassertion 5y ago
My assumptions are based on study and experience. My "Zealotry" is just a desire to reduce harm to users in an area that I personally believe we should strive not to regress on. I'm not interested in discussing Rust. Frankly, I'm sure there will be plenty of other people already doing so. What's clear from this thread is that Hare does attempt to move the needle, relative to C, with regards to safety. My opinion is that that's not enough for the use cases they're targeting, but I suppose it's really up to whoever's writing the software to decide that.
kaba0 5y ago
> A simpler language makes this more possible This is false. Rust’s borrow checker is nothing else but an included proof assistant for rust code. The reason it can catch so many memory issues and data races is specifically due to a more restricted language. Also, sel4 is a relatively tiny program which was written for an unusually long time by domain experts. Formal verification simply doesn’t scale to global properties, that’s why some restrictions are useful as they allow local reasonings instead. For a more hands-on example look at the quality of auto-complete in case of Intellij’s Java vs a dynamically typed language. This night and day difference in quality is yet again possible due to what the language can’t denote. Re rust macros: I don’t get your point, AFAIK they simply expand to regular old Rust code and then gets compiled, so the exact same safety guarantees apply.
- Shared404 5y ago
  > > discovery of other forms of security regression, like timing or energy side channels. > so the exact same safety guarantees apply. I see this a lot with Rust, and with encryption. There are no magic bullets. There is no "you are safe because you used this" tool. In this case, Rust's safety gaurantees apply only to memory safety. GP wasn't talking about memory safety above.
  - kaba0 5y ago
    Sure, and I do share your concern regarding over ambitious claims on rust’s safety benefits, but I just don’t get why would a macro hide these any more than let’s say another function call would. I don’t mean to say that a macro can’t get needlessly complex, but the same is true of functions that are inherent in basically any language. In the worst case macros can be expanded and looked at in their full forms. They are as always abstractions, which are pretty much necessary, but they can be abused as well.
- throwawaymaths 5y ago
  > Formal verification simply doesn’t scale to global properties This is an assertion you are making with absolutely no evidence, and also totally self-contradictory with your statement "Rust’s borrow checker is nothing else but an included proof assistant for rust code". While we're at it, also Ada does this, which has long been used for large scale mission critical applications where formal assurances are necessary (with even more available optional safeties than rust provides).
  - zozbot234 5y ago
    Formal verification doesn't scale to global properties in the general case. Global properties that are simple and type-like (in that they match the syntactic structure of the program in a fully "compositional" way, like Rust lifetimes) can be checked with comparable ease. Complex properties can often be checked within a single, self-contained, small-enough program module. Trying to do both at the same time - check complex properties globally - is highly problematic. That's why the Rust borrow checker has to make simplifying assumptions, and use 'unsafe' as an escape hatch.
HelloNurse 5y ago
"Optional" means unused or misused until proved otherwise. No checking and no guarantees can be assumed, and if someone tries to deploy an add-on proof assistant I'd expect managers to see programmers who waste time pursuing some warnings instead of making progress on new features.
- throwawaymaths 5y ago
  This is wholly unimaginative, there is a wide window of usage patterns that are not "unused or misused", for example, on by default but off with a project flag, or off when building a dev release but on when building a prod release, and also don't forget my point that many projects simply don't need the level of memory safety that rust provides. For example if you are single threaded and never free, or if you have an arena strategy.
  - HelloNurse 5y ago
    Reducing concurrency and/or dynamic memory management makes a program easier to reason about for the compiler (and more likely to be correct in practice), not less in need of correct memory management. I'm "wholly unimaginative" about what variables can be acceptably corrupted; I can only think of deliberately reading uninitialized memory as a randomness source, a case that is easier to prevent (by clearing allocated memory by default on the OS side) than to enable.
xavxav 5y ago
> It could be baked into proof assistants that are part of (optional or add-on) tooling, like what sel4 does. A simpler language makes this more possible, and the things that a proof assistants can do go far beyond what rust is able to provide I’m actually doing my PhD on the verification of Rust programs and wanted to add that the opposite is actually true. The type system of Rust helps to create a much simpler model of the language which allows us to do proofs in much larger scale than with C (for the same effort). This is specifically because of how ownership typing helps us simplify reasoning.

staticassertion 5y ago

My assumptions are based on study and experience. My "Zealotry" is just a desire to reduce harm to users in an area that I personally believe we should strive not to regress on. I'm not interested in discussing Rust. Frankly, I'm sure there will be plenty of other people already doing so. What's clear from this thread is that Hare does attempt to move the needle, relative to C, with regards to safety. My opinion is that that's not enough for the use cases they're targeting, but I suppose it's really up to whoever's writing the software to decide that.

kaba0 5y ago

> A simpler language makes this more possible This is false. Rust’s borrow checker is nothing else but an included proof assistant for rust code. The reason it can catch so many memory issues and data races is specifically due to a more restricted language. Also, sel4 is a relatively tiny program which was written for an unusually long time by domain experts. Formal verification simply doesn’t scale to global properties, that’s why some restrictions are useful as they allow local reasonings instead. For a more hands-on example look at the quality of auto-complete in case of Intellij’s Java vs a dynamically typed language. This night and day difference in quality is yet again possible due to what the language can’t denote. Re rust macros: I don’t get your point, AFAIK they simply expand to regular old Rust code and then gets compiled, so the exact same safety guarantees apply.

Shared404 5y ago
> > discovery of other forms of security regression, like timing or energy side channels. > so the exact same safety guarantees apply. I see this a lot with Rust, and with encryption. There are no magic bullets. There is no "you are safe because you used this" tool. In this case, Rust's safety gaurantees apply only to memory safety. GP wasn't talking about memory safety above.
- kaba0 5y ago
  Sure, and I do share your concern regarding over ambitious claims on rust’s safety benefits, but I just don’t get why would a macro hide these any more than let’s say another function call would. I don’t mean to say that a macro can’t get needlessly complex, but the same is true of functions that are inherent in basically any language. In the worst case macros can be expanded and looked at in their full forms. They are as always abstractions, which are pretty much necessary, but they can be abused as well.
throwawaymaths 5y ago
> Formal verification simply doesn’t scale to global properties This is an assertion you are making with absolutely no evidence, and also totally self-contradictory with your statement "Rust’s borrow checker is nothing else but an included proof assistant for rust code". While we're at it, also Ada does this, which has long been used for large scale mission critical applications where formal assurances are necessary (with even more available optional safeties than rust provides).
- zozbot234 5y ago
  Formal verification doesn't scale to global properties in the general case. Global properties that are simple and type-like (in that they match the syntactic structure of the program in a fully "compositional" way, like Rust lifetimes) can be checked with comparable ease. Complex properties can often be checked within a single, self-contained, small-enough program module. Trying to do both at the same time - check complex properties globally - is highly problematic. That's why the Rust borrow checker has to make simplifying assumptions, and use 'unsafe' as an escape hatch.

HelloNurse 5y ago

"Optional" means unused or misused until proved otherwise. No checking and no guarantees can be assumed, and if someone tries to deploy an add-on proof assistant I'd expect managers to see programmers who waste time pursuing some warnings instead of making progress on new features.

throwawaymaths 5y ago
This is wholly unimaginative, there is a wide window of usage patterns that are not "unused or misused", for example, on by default but off with a project flag, or off when building a dev release but on when building a prod release, and also don't forget my point that many projects simply don't need the level of memory safety that rust provides. For example if you are single threaded and never free, or if you have an arena strategy.
- HelloNurse 5y ago
  Reducing concurrency and/or dynamic memory management makes a program easier to reason about for the compiler (and more likely to be correct in practice), not less in need of correct memory management. I'm "wholly unimaginative" about what variables can be acceptably corrupted; I can only think of deliberately reading uninitialized memory as a randomness source, a case that is easier to prevent (by clearing allocated memory by default on the OS side) than to enable.

xavxav 5y ago

> It could be baked into proof assistants that are part of (optional or add-on) tooling, like what sel4 does. A simpler language makes this more possible, and the things that a proof assistants can do go far beyond what rust is able to provide I’m actually doing my PhD on the verification of Rust programs and wanted to add that the opposite is actually true. The type system of Rust helps to create a much simpler model of the language which allows us to do proofs in much larger scale than with C (for the same effort). This is specifically because of how ownership typing helps us simplify reasoning.