4 ms·

I've seen that before - is there an implementation, and also, how do the usual users of Ada feel about it? I feel like one of the attractions to Ada for this s

by geofft 6y ago

I've seen that before - is there an implementation, and also, how do the usual users of Ada feel about it? I feel like one of the attractions to Ada for this sort of use case is its maturity, and "here's a proposal for a complicated feature, inspired by Rust, a language which young and rapidly evolving and in particular switched to a new borrow checker implementation less than two years ago and shipped it with known unsoundnesses and is working on a new borrow checker implementation as we speak" may not be attractive to Ada's usual users. :) (To be clear, I'm fine with the risk profile of Rust's borrow checker, but in part that's because I'm fine with the risk profile of using the latest stable Rust and picking up any fixes every six weeks. I'm fine with a more powerful feature that lets me develop code quickly and I'm fine with upgrading my compiler every six weeks to pick up any bug fixes; I imagine that people writing airplane control software are probably going to prefer something less powerful that hasn't changed in decades.) Honestly, I think one of the questions here is community. I don't really know who the Ada community is, beyond press releases from Adacore about planes and trains. I suspect that community simply does not care about safe dynamic allocation, even if it were available as a supported option, so they aren't going to be excited about testing out this feature. Is there a user community who would use this, in production (doesn't have to be a company, the "serious hobbyist" open source dev is fine and probably even preferable here), within the next five years or so? Are there folks writing stuff like high-performance grep replacements in Ada or hardened HTML 5 implementations in Ada? I'd love to see (or help with!) such a comparison, but I get the sense that Ada's and Rust's use cases are so different that writing a fair apples-to-apples comparison is hard and even finding someone to do it would be hard.

EdPF 6y ago
There's a telegram group https://t.me/ada_lang https://t.me/ada_lang you could open that question on. Also, there's work (I think on GitLab) on a package manager called Alire. And the very old standby comp.lang.ada which tends to have some interesting conversations.
EdPF 6y ago
Whoops, forgot. The borrow checking memory management is available on GNAT Community Edition 2020, for SPARK and (I believe) also Ada itself. The GNAT Ada compiler is used to compile and build SPARK apps. Since SPARK is very strict, the implementation is robust even at this relatively early stage.
Rochus 6y ago
Where is the quoted text from ("here's a proposal... as we speak")? > I imagine that people writing airplane control software are probably going to prefer something less powerful that hasn't changed in decades True, depending on the design assurance level a certified compiler is required. > I suspect that community simply does not care about safe dynamic allocation See the reference in my former post. Whether and when the certification authorities accept it is yet another question. > Is there a user community who would use this, in production ... It's easy to find projects on Github where dynamic allocation is used; e.g. https://github.com/ghdl/ghdl; https://github.com/ghdl/ghdl; with the current developments, such applications may also have a chance for formal verification in the future. And no doubt it would help if the Rust compiler was formally verified as well.
- MaxBarraclough 6y ago
  > it would help if the Rust compiler was formally verified as well As far as I know, the only usable formally-verified compiler (for a serious programming language) is the CompCert C compiler. Even C compilers and Ada compilers intended for use with critical systems, don't tend to be formally verified. Of course, it would still be great if the compiler for Rust (or Ada, or any other language for that matter) could be formally verified. It's unfortunate that CompCert isn't Free Software.
  - Rochus 6y ago
    The Rust compiler had some severe bugs in the past which undermined the effectiveness of the memory safety. There is the saying in software engineering that the number of undiscovered errors in the system is proportional to the number of discovered errors. On the other hand Ada compilers used to be subjected to strict validation procedures in the past, and the AdaCore toolchain has an ISO 26262 and IEC 61508 qualification. That was the source of my remark.
    - MaxBarraclough 6y ago
      Ok, but a formally verified compiler is a very different beast from a high quality compiler. We can realistically hope the Rust compiler team significantly improve the correctness of the compiler, but full formal verification is unlikely. CompCert is an extremely impressive achievement, and compiles a near-complete subset of standard C. A verified Rust compiler would be an enormous undertaking, and would need a very skilled team. It also wouldn't be worth trying unless the Rust language were very stable, which, if I understand correctly, it isn't.

by geofft 6y ago

EdPF 6y ago

There's a telegram group https://t.me/ada_lang https://t.me/ada_lang you could open that question on. Also, there's work (I think on GitLab) on a package manager called Alire. And the very old standby comp.lang.ada which tends to have some interesting conversations.

EdPF 6y ago

Whoops, forgot. The borrow checking memory management is available on GNAT Community Edition 2020, for SPARK and (I believe) also Ada itself. The GNAT Ada compiler is used to compile and build SPARK apps. Since SPARK is very strict, the implementation is robust even at this relatively early stage.

Rochus 6y ago

Where is the quoted text from ("here's a proposal... as we speak")? > I imagine that people writing airplane control software are probably going to prefer something less powerful that hasn't changed in decades True, depending on the design assurance level a certified compiler is required. > I suspect that community simply does not care about safe dynamic allocation See the reference in my former post. Whether and when the certification authorities accept it is yet another question. > Is there a user community who would use this, in production ... It's easy to find projects on Github where dynamic allocation is used; e.g. https://github.com/ghdl/ghdl; https://github.com/ghdl/ghdl; with the current developments, such applications may also have a chance for formal verification in the future. And no doubt it would help if the Rust compiler was formally verified as well.

MaxBarraclough 6y ago
> it would help if the Rust compiler was formally verified as well As far as I know, the only usable formally-verified compiler (for a serious programming language) is the CompCert C compiler. Even C compilers and Ada compilers intended for use with critical systems, don't tend to be formally verified. Of course, it would still be great if the compiler for Rust (or Ada, or any other language for that matter) could be formally verified. It's unfortunate that CompCert isn't Free Software.
- Rochus 6y ago
  The Rust compiler had some severe bugs in the past which undermined the effectiveness of the memory safety. There is the saying in software engineering that the number of undiscovered errors in the system is proportional to the number of discovered errors. On the other hand Ada compilers used to be subjected to strict validation procedures in the past, and the AdaCore toolchain has an ISO 26262 and IEC 61508 qualification. That was the source of my remark.
  - MaxBarraclough 6y ago
    Ok, but a formally verified compiler is a very different beast from a high quality compiler. We can realistically hope the Rust compiler team significantly improve the correctness of the compiler, but full formal verification is unlikely. CompCert is an extremely impressive achievement, and compiles a near-complete subset of standard C. A verified Rust compiler would be an enormous undertaking, and would need a very skilled team. It also wouldn't be worth trying unless the Rust language were very stable, which, if I understand correctly, it isn't.