Rust graduates from meme language state

Rust is no longer just a meme language, it now has an actual proof that it's safe: people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf

It's too hard!
I'm too retarded!
C++ can do everything Rust can anyway!

Who gives a shit about some academic bullshit? There are lots of papers written about haskell and no-one uses that for anything useful.

You mean rust turned from meme language into academic meme language. Shit now we don't compare it to sepples we compare it haskell.

this to be sincere.

redpill me on haskell. is it worth spending ~100hours?

doesn't matter it's still run by raging communists

>What happened
Some guy looked at like 3 things in the standard library and proved who knows what properties

>What Rustfags will pretend that happened
Rust is guaranteed to be bug-free and 1 compilation = 1 formal verification

Cpeepee BTFO

Now this damage control of yours is pretty embarrassing

Nice arguments you got there. You might want to go back to /r/rust and write a celebratory comment that uses the word 'safety' at least 9 times.

As someone who comes from Java, I have a certain level of expectation for what tooling, documentation, and libraries are available.

And a lot of these depend on the community. We didn't get Joda Time/Money because we had a shit community.

Has Rust got a community of people who make good stuff yet?

Because editor-only isn't good enough for writing large stuff in. I'm fine with using Make for building and some funky ODBC stuff to talk to a db with, etc. But there better be more to a language than sublime Hello World and FizzBuzz implementations.

Think of it as learning how to think in a functional way. IOW, when all the good ideas are pilfered and put into Enterprise languages that you use in your 9-5 job, you'll be way ahead, and your boss will be impressed.

They proved a good portion of the type system but as stated in the paper's conclusion, there's still some parts that aren't included in its model and IMO, they seem to be pretty important from a soundness standpoint.

>We had to make some concessions in our modeling: We do not model (1) more relaxed forms of atomic accesses, which Rust uses for efficiency in libraries like Arc ; (2) Rust’s trait objects (comparable to interfaces in Java), which can pose safety issues due to their interactions with lifetimes; or (3) stack unwinding when a panic occurs, which causes issues similar to exception
safety in C++ [2]. We proved safety of the destructors of the verified libraries, but do not handle automatic destruction, which has already caused problems [11] for which the Rust community still does not have a modular solution [58]. The remaining omissions are mostly unrelated to ownership, like traits (Rust’s take on type classes) and type-polymorphic functions.

The proof of rust's soundness is kind of irrelevant in my opinion because it really only reinforces the safety standpoint of the language which not many people dispute about the language since it was very well designed in that area. It has bigger issues with things like verbosity, interfacing with C++, and missing low level C-replacement kind of things like aligned memory and unions, although I think the latter is getting in soon.

Why would you learn Rust anyway when we already have many programming languages which are accepted by the industry? Serious question

Syntax is still shit to so I'll stick with C or C-style languages.
But I'm glad all the feminists of github will be able to write their KillAllWhiteMales.bin in a now truly safe space language.

You don't even understand anything about that proof

Good balance of safety and security

See

I 100% completely understand it actually

>Who gives a shit about some academic bullshit?
This is the first good thing to happen about rust.
Before this it was just some bullshit some communist faggot pulled out of his ass.
Now it has a sturdy foundation that mathematically shows it's a valid programming model.

>Some guy looked at like 3 things in the standard library and proved who knows what properties
who knows what properties?
stop playing the fool.

He proved THE gold standard theorems that are required for any type system. It means that they mathematically know that when you execute a rust program that didn't have compiler errors the program will run correctly without misinterpreting data and produce a valid result.

You are right. This isn't 100% of rust but it's a serious chunk. This is very significant and shows the core model behind the language is actualy solid and not just some broken crap.

>The proof of rust's soundness is kind of irrelevant in my opinion because it really only reinforces the safety standpoint of the language which not many people dispute about the language
that's because everyone interested in rust was a bandwagoning unthinking sheep. Now that the PL itself has been mathematical studied and proved valid grown ups might start to use it.

I couldn't agree more. People should have been using Ada for decades. All of GNU userland should be implemented in it. But they just didn't.

bump

Fuck off with your meme language, shill.

We already had this thread, fuck off.

archive link?

"I use paper to wipe my butt every morning. That's how much paper is worth" - Linus