5 ms·

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

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 8y ago
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/html/Rat-3-2.html 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
- galangalalgol 8y ago
  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.
  - johnisgood 8y ago
    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.
  - henrikeh 8y ago
    >> [...] 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 8y ago
      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 8y ago
        Many planes, trains, rockets and medical devices run on Ada. There is more to commercial compilers than winning the benchmarks game.
        Narishma 8y ago
        Those things don't need to be particularly fast. What they need is consistent and predictable performance and resource usage.
        galangalalgol 8y ago
        Planes trains and rockets have more sensors than ever and speed is very important.
        deleted 8y ago
        [deleted]
        galangalalgol 8y ago
        Most of my experience is embedded c++ but I have written ada rust and a fair bit of jovial73. Rust is a perfect fit for those same domains. Most o the things that ran Ada in the US have now switched to c++. Do178b certified safety critical c++ is a horrible thing to develop. I'm hoping rust comes in to fix that.
- Yoric 8y ago
  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/ 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 8y ago
    SPARK is a subset of Ada 2012. Your examples are possible with contracts.
    - Yoric 8y ago
      I'm interested, do you have examples somewhere on how to implement that kind of properties with contracts?
      - yannickmoy 8y ago
        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 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/newdev_04_dross.pdf 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);

johnisgood 8y ago

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/html/Rat-3-2.html 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

galangalalgol 8y ago
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.
- johnisgood 8y ago
  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.
- henrikeh 8y ago
  >> [...] 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 8y ago
    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 8y ago
      Many planes, trains, rockets and medical devices run on Ada. There is more to commercial compilers than winning the benchmarks game.
      - Narishma 8y ago
        Those things don't need to be particularly fast. What they need is consistent and predictable performance and resource usage.
        galangalalgol 8y ago
        Planes trains and rockets have more sensors than ever and speed is very important.
        deleted 8y ago
        [deleted]
      - galangalalgol 8y ago
        Most of my experience is embedded c++ but I have written ada rust and a fair bit of jovial73. Rust is a perfect fit for those same domains. Most o the things that ran Ada in the US have now switched to c++. Do178b certified safety critical c++ is a horrible thing to develop. I'm hoping rust comes in to fix that.
Yoric 8y ago
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/ 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 8y ago
  SPARK is a subset of Ada 2012. Your examples are possible with contracts.
  - Yoric 8y ago
    I'm interested, do you have examples somewhere on how to implement that kind of properties with contracts?
    - yannickmoy 8y ago
      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 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/newdev_04_dross.pdf 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);