[gameswithgo]

>could you please tell me what kind of official formal proof tools exist for Rust that makes it predictable?

I feel like you aren't really asking a question, that your intent was really to lecture someone, but in case you really are:

* a borrow checker * option types

So OCaml would catch a similar set of obvious errors, though Rust would also catch all data races at compile time, as the borrow checker does that as well as prevent memory mistakes.

[johnisgood]

No, I was really curious. My bad if it looked like I was trying to lecture. I do not think that I have the necessary knowledge in this topic to do that. :)

> a borrow checker

What exactly do you mean? How does it differ from any other language's type system?

> would also catch all data races at compile time

In Ada/SPARK, you can formally verify tasks, too. Please take a look at https://docs.adacore.com/spark2014-docs/html/ug/en/source/co... if you have some time!

> prevent memory mistakes.

Which mistakes are you referring to specifically? I need to know so I can have a meaningful response to it, but all I can say right now is that Ada/SPARK does the same.

[masklinn]

> > a borrow checker

> What exactly do you mean? How does it differ from any other language's type system?

Part of rust's type system is sub-structural: by default, Rust's types are affine, which means you can only use them once (at most, not exactly).

Now this is not super convenient to use and could have efficiency issues (e.g. any time you want to check a value in a structure you'd have to return the structure so the caller can get it back), so to complement this you can borrow (create a reference). The borrow checker is the bit which checks that borrows satisfy a bunch of safety rules, mostly that a borrow can't outlive its source, and that you can have a single mutable borrow or any number of immutable borrows concurrently.

The borrow checker provides for memory-safe pointers to or into a structure you're not the owner of, with no runtime cost.

[Yoric]

> What exactly do you mean? How does it differ from any other language's type system?

If you're familiar with affine types, this is basically what Rust's borrow checker implements.

If you're not familiar, it's a bit complicated to summarize on Hacker News. You should try it out, because it lets you guarantee statically entire classes of properties that non-academic languages struggle with.

> In Ada/SPARK, you can formally verify tasks, too. Please take a look at https://docs.adacore.com/spark2014-docs/html/ug/en/source/co.... if you have some time!

I'm not an expert in Ada, but yes, that's pretty similar to some of the properties Rust will let you check out of the box.

edit My memory of Ada was incorrect.

[Manishearth]

It's more than just affine types, it's region typing, which is far less common.

[Yoric]

Fair enough.

[int_19h]

Can you recommend a good book on SPARK in general? I've read one on Ada 2012 itself, and what it had to say about Ravenscar and SPARK got me interested.

[pjmlp]

"Building High Integrity Applications with SPARK"

There is also "High Integrity Software: The SPARK Approach to Safety and Security", I never read it, but it is written by a well known author in the Ada community.

[johnisgood]

Yes, and also: https://learn.adacore.com/courses/intro-to-spark/index.html