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.
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.
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).
And I don’t believe my claim is unsupported, the largest formally verified program is the mentioned sel4, which is still tiny compared to even the smallest of business apps and was written by domain experts over multiple years.
Restricting a problem to a subset is like the numero uno step to solve any hard problem - and this is what rust basically mandate. It won’t provide bug-free programs, but it can reliably prove the absence of memory bugs and data races due to the borrow checker, which can do its work on function-scope, since all the relevant information is encoded in the function’s generic lifetime arguments.
Proof assistance is sort of irrelevant. Types and proofs are related, as denoted by the curry howard correspondance.
The real issue with "throwawaymaths"' point is that they're saying "use proof assistants" to people who are using proof assistants. SEL4 is a terrible example of a success story, as it took ages to complete, and then there was immediately a bug found in a class they weren't looking for - because rice's theorem.
They're clearly advocating for the use of specific and explicit proof assistants, which is fine and a totally reasonable thing to advocate for, but in no way is related to rust or the discussion, which is why I chose not to engage.
> 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.
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.
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.
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.
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.