News for hackers. Stuff that matters.
Re:Microsoft: Rust Is the Industry’s ‘Best Chance’ at Safe S... by nilkn on Saturday June 13, 2020 @02:33PM (#23511540)
> Lots of unsafe code is safe.

This seems like a weird statement to make to me when defending Rust simultaneously. The whole selling point of Rust is that it's supposed to let you write provably safe code. When "unsafe" is used, what you're writing can no longer be proven as safe by the compiler. Maybe you've convinced yourself it's actually safe via some other argument, but people have been convincing themselves that their code is memory safe for decades and they're often wrong. More insidiously, relying on anything in Rust that uses "unsafe" makes it seem like the compiler is proving your own code is safe, but that is no longer true.

With that said, I don't really disagree with what I think your main point is. But seeing unsafe code in Rust is similar to seeing unsafePerformIO in Haskell libraries. Both of these are much more common than the languages' respective evangelists would have you believe, and at some point it actually does start to call into question whether the languages are successful at their basic design goals. (Spoiler: I believe that they are successful more than they are not, and even in the face of the proliferation of "unsafe" code in both languages, they're still worth using.)

Re:Microsoft: Rust Is the Industry’s ‘Best Chance’ at Safe S... by staticassertion on Saturday June 13, 2020 @03:14PM (#23511876)
> The whole selling point of Rust is that it's supposed to let you write provably safe code.

I disagree. A significant purpose of rust is to encapsulate unsafe code, and provide safe abstractions. Lots of unsafe code is safe - most of it, even, I'd bet.

Re:Microsoft: Rust Is the Industry’s ‘Best Chance’ at Safe S... by nilkn on Saturday June 13, 2020 @03:23PM (#23511942)
> Lots of unsafe code is safe

I mean this with the greatest possible respect, but you replied by simply restating verbatim the quote that I originally responded to, so I'll just point you to my previous post.

Re:Microsoft: Rust Is the Industry’s ‘Best Chance’ at Safe S... by SAI_Peregrinus on Saturday June 13, 2020 @03:54PM (#23512181)
`unsafe` the keyword vs unsafe the concept. Lots of `unsafe` code is safe when used through a safe wrapper. Verifying that is the duty of the programmer. The compiler can't prove it, but quite often the programmer can.

IMO it's good practice to provide a comment with such proof for every `unsafe` block.

So `unsafe` does not imply unsound, but unsound does imply `unsafe`.

Re:Microsoft: Rust Is the Industry’s ‘Best Chance’ at Safe S... by staticassertion on Saturday June 13, 2020 @04:30PM (#23512425)
This is what I was trying to say. Unsafe doesn't imply exploitability, at all.
Re:Microsoft: Rust Is the Industry’s ‘Best Chance’ at Safe S... by staticassertion on Saturday June 13, 2020 @03:25PM (#23511958)
Sorry if I misunderstood your post then.
Re:Microsoft: Rust Is the Industry’s ‘Best Chance’ at Safe S... by zozbot234 on Saturday June 13, 2020 @02:43PM (#23511631)
The compiler has very limited "proof" capabilities even in principle, especially wrt. unsafe{} code. From a principled POV it would be nice to be able to provide a formal, compiler-checked proof that some block of code that has to rely on "unsafe" operations doesn't actually violate the language safety guarantees and can be wrapped safely. But this will have to depend on a formal model of "unsafe" itself which is still lacking. And it wouldn't even help for things like FFI, which involves calls into outside code for which the semantics are not formally known.