[johnisgood]

> before but soon got annoyed with obvious errors that would only show up once you run a program.

From what I gather you are comparing static vs dynamic typing, and I agree. I do not use Python because I prefer a subset of errors caught at compile-time. However, it is silly to make it sound like that this is somehow limited to Rust. You could just as well have used Go or OCaml and feel "refreshed" because obvious errors would have been caught at compile-time.

> The predictable nature of Rust

Again, given the context, it is static vs dynamic typing. This is not something limited to Rust. In case you were not talking about static typing and its pros, could you please tell me what kind of official formal proof tools exist for Rust that makes it predictable?

[atoav]

Sorry if I angered you. I never claimed that Rust was the only language that has these properties.

My experience was is: I have never seen a language/environment where these rules were so well thought out, so well communicated and so well enforced. The package managment works like a charm, the module system (since edition 2018) is the best I have seen etc.

These are all subjective – I am a film/philosophy student who codes and I never received any formal education on any CS related topic. I was speaking about why Rust feels sound to me. Good chances Haskell will look sound to me too, very good chance I might check out more CS topics. No hard feelings please.

[johnisgood]

It is fine, and no it didn't anger me, so no need to apologize, really. :)

> I never claimed that Rust was the only language that has these properties.

Yeah, that is my mistake. Sorry for misunderstanding you!

> I never received any formal education on any CS related topic

Same here actually! :P

> No hard feelings please.

Not at all!

I understand that you like coding in Rust, and that is completely okay with me, and even if it was not, that should not deter you from continuing what you are doing.

[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

[matthewmacleod]

That’s one aspect of the errors that are avoided, but there are many others too - some of which aren’t solved by other languages. Go, for example, will happily nail through all of your obviously null pointers with gay abandon. The Rust ownership model prevents other classes of bugs.

It’s not a panacea—and to be blunt, I find Rust more work than it is worth for the sort of projects I typically work on. But any tools which can eliminate whole error categories are worth looking at for sure!

[johnisgood]

I was responding to the issue I quoted, which really is just a matter of using a programming language with static typing. :)

> some of which aren’t solved by other languages

You only mentioned null pointers, so I will go with that. In Ada, you can have access types (pointers) that are guaranteed to not be null, and accessibility rules of Ada prevent dangling references to declared objects or data that no longer exists, so this particular issue is solved by a language other than Rust. Please feel free to give me other examples of errors or issues that you may believe is not solved by languages other than Rust.

https://www.adaic.org/resources/add_content/standards/05rat/...

> But any tools which can eliminate whole error categories are worth looking at for sure!

I agree. That is why I think Ada/SPARK is awesome! :P

[Yoric]

I will give you a few examples. My knowledge of Ada is insufficient, so I'll let you tell me whether Ada can solve that without using an external prover (note: being able to use an external prover is great and I haven't seen this done in Rust yet :) – but that's not the topic at hand).

1/ Consider a file `f` (or a socket, etc.). Using the standard library, Rust will statically ensure that, once the file is closed, you cannot attempt to, say, read from it. This is nothing special to files, just an aspect of the borrow checker.

2/ Consider a communication protocol. You need to send a message `HLO`, expect a message `ACK`, then send something else, etc. It is pretty easy to design your objects such that the operations of sending the message, receiving the message, etc. will change the type of your protocol object, ensuring statically that you never send/expect a message that you're not supposed to send in the current state.

If you're curious, I wrote a blurb last year on the topic: https://yoric.github.io/post/rust-typestate/

3/ I quickly googled "Ada spark phantom types" and didn't find anything. Does Ada support phantom types?

[pjmlp]

SPARK is a subset of Ada 2012.

Your examples are possible with contracts.

[Yoric]

I'm interested, do you have examples somewhere on how to implement that kind of properties with contracts?

[yannickmoy]

You can look at this blog post where I used a ghost global variable to hold the current state of the game (see section "Proving Functional Properties of Tetris Code"): https://blog.adacore.com/tetris-in-spark-on-arm-cortex-m4

You can similarly express ghost properties of your types, even though we don't have ghost fields in SPARK. For more on ghost code in SPARK, you can look at this presentation last year from my colleague Claire Dross: https://www.adacore.com/uploads/products/SSAS-Presentations/...

As a more extensive example of a useful library with this kind of contracts for proof, Joffrey Huguet added rich contracts of this kind to the Ada.Text_IO standard library just two weeks ago, as part of his current internship with us. This should be in the FSF trunk in the coming weeks. For example, here are some contracts he added:

   procedure Open
     (File : in out File_Type;
      Mode : File_Mode;
      Name : String;
      Form : String := "")
   with
     Pre    => not Is_Open (File),
     Post   =>
      Is_Open (File)
      and then Ada.Text_IO.Mode (File) = Mode
      and then (if Mode /= In_File
                  then (Line_Length (File) = 0
                        and then Page_Length (File) = 0)),
     Global => (In_Out => File_System);

   procedure Put (File : File_Type; Item : Character) with
     Pre    => Is_Open (File) and then Mode (File) /= In_File,
     Post   =>
       Line_Length (File)'Old = Line_Length (File)
       and Page_Length (File)'Old = Page_Length (File),
     Global => (In_Out => File_System);

   procedure Close  (File : in out File_Type) with
     Pre    => Is_Open (File),
     Post   => not Is_Open (File),
     Global => (In_Out => File_System);

[galangalalgol]

Ada is awesome, and if compiler writers had been more timely it might have taken hold. Rust solves the same problems without a runtime, and about 3 times the performance. Granted it looks like c++ and ocaml made a particularly ugly child.

[henrikeh]

>> [...] solves the same problems without a runtime, and about 3 times the performance.

I think you should look more into Ada. The only "runtime" is for the exception handling and bounds checking, both of which can be turned off if needed.

And I don't know where you got that "3 times" figure from? Do you have an example you are referring to?

[galangalalgol]

I knew you could turn off the runtime but not about the formal verification lint tools that make it safe to do so. My reference for performance is the benchmark game. If you or someone else can mod those programs to beat rust I'd be thrilled. I like Ada.

[pjmlp]

Many planes, trains, rockets and medical devices run on Ada.

There is more to commercial compilers than winning the benchmarks game.

[johnisgood]

I believe the performance differences on The Computer Language Benchmarks Game is largely due to the implementations themselves. For one, pidigits have been translated from Pascal to Ada using p2ada. I do not think that this is a fair comparison at all.

[johnisgood]

Which problems are you referring to?

You can do everything that has been mentioned without Ada's RTS, you can also disable all run-time checks. You can use static analysis tools (there are many, and available for free), for example, you can formally verify the correctness of the program, no run-time checks required.

[outworlder]

This is not only static vs dynamic typing. Rust provides a set of abstractions seldom found elsewhere. The borrow checker, for instance.

It is more a question of semantics.

[c3534l]

I assumed borrowing and lifetimes were part of his experience as well.

[atoav]

Sure, and I find both not very hard as a concept.

The hard thing is not understanding the concepts but learning what this implies for your coding style, especially when you come from a garbage collected language like Python.

Both concept can at times give you hard to solve tasks, but it usually is because the problem you are trying to solve is hard and you cannot just naively hack away without thinking long and hard about it.

Other than that I learned liking the borrow checker and lifetimes because you will get a incredible narrow scope of which variables can matter when — which makes debugging much easier

[jhrmnn]

And with something like Mypy, you can get most of the benefits of static typing even in Python, if you want to. But Rust has so much more to offer, such as memory ownership.

[atoav]

I didn’t know mypy, but I am going to check it out, thanks!