4 ms·

I for one as someone who programmed professionally in both Ocaml and Ada still don’t see where Rust is supposed to fit. If I was doing something high level, I

I for one as someone who programmed professionally in both Ocaml and Ada still don’t see where Rust is supposed to fit. If I was doing something high level, I would probably use Ocaml which has nicer features. If I wanted to write safe code, Ada offers a better experience with the availability of SPARK for parts I would probably end up wanting to prove. If I just want to write concurrent code with the certainty I could find someone to maintain it, Go seems the way to go. Rust seems to want to be a replacement for Ada but seems to actually attract programmers used to high level language chasing the hype. What’s the story with Rust and verification nowadays?

qznc 4y ago
I think Rust has a good chance to take away market share from Ada and Ocaml. Its eco system (packages, documentation) is more comprehensive already thanks to its broader appeal and being in fashion. I don’t see why stronger verification should not appear at some point. Progress and need is there.
School-Cotton 4y ago
Rust is supposed to be a better C++, and resoundingly succeeds at that goal.
- pjmlp 4y ago
  It partially succeeds at that, because while it has a much better story in being safe by default, there are plenty of C++ use cases where Rust still hasn't a story to sell. HPC, HFT, GPGPU, LLVM/GCC infrastructure, GUI, console SDKs, drivers SDKs, security certification ,....
  - School-Cotton 4y ago
    Ok, fair, you’re right. Rust is successful in a rather large subset of C++ niche, but not yet the whole thing!
  - adgjlsfhk1 4y ago
    imo, Julia is a better fit than rust or C++ for hpc/gpgpu
    - pjmlp 4y ago
      It might someday, still lots of room to improvement regarding current workloads. I not not seeing Fermilab or CERN doing real time beam processing in Julia anytime soon. Or stuff like having graphical shader debugging tools for Julia.
      - adgjlsfhk1 4y ago
        Julia already is starting to be used for high energy physics (see https://arxiv.org/pdf/2003.11952.pdf https://arxiv.org/pdf/2003.11952.pdf and https://www.youtube.com/watch?v=QlfAa-LN1SA https://www.youtube.com/watch?v=QlfAa-LN1SA for details). It's definitely not the default yet, but there absolutely is effort to use it for particle accelerators.
thesuperbigfrog 4y ago
>> What’s the story with Rust and verification nowadays? It is in progress but likely several years to go before a MVP is released. Ferrocene [1] is the primary effort that I am aware of and that seems to be making progress towards a verified rustc suitable for safety critical work. Ferrous Systems is working with AdaCore and just released the Ferrocene Language Specification [2] to formally document the Rust subset that Ferrocene will use. [1] https://ferrous-systems.com/ferrocene/ https://ferrous-systems.com/ferrocene/ [2] https://ferrous-systems.com/blog/ferrocene-language-specification/ https://ferrous-systems.com/blog/ferrocene-language-specific...
deleted 4y ago
[deleted]

qznc 4y ago

I think Rust has a good chance to take away market share from Ada and Ocaml. Its eco system (packages, documentation) is more comprehensive already thanks to its broader appeal and being in fashion. I don’t see why stronger verification should not appear at some point. Progress and need is there.

School-Cotton 4y ago

Rust is supposed to be a better C++, and resoundingly succeeds at that goal.

pjmlp 4y ago
It partially succeeds at that, because while it has a much better story in being safe by default, there are plenty of C++ use cases where Rust still hasn't a story to sell. HPC, HFT, GPGPU, LLVM/GCC infrastructure, GUI, console SDKs, drivers SDKs, security certification ,....
- School-Cotton 4y ago
  Ok, fair, you’re right. Rust is successful in a rather large subset of C++ niche, but not yet the whole thing!
- adgjlsfhk1 4y ago
  imo, Julia is a better fit than rust or C++ for hpc/gpgpu
  - pjmlp 4y ago
    It might someday, still lots of room to improvement regarding current workloads. I not not seeing Fermilab or CERN doing real time beam processing in Julia anytime soon. Or stuff like having graphical shader debugging tools for Julia.
    - adgjlsfhk1 4y ago
      Julia already is starting to be used for high energy physics (see https://arxiv.org/pdf/2003.11952.pdf https://arxiv.org/pdf/2003.11952.pdf and https://www.youtube.com/watch?v=QlfAa-LN1SA https://www.youtube.com/watch?v=QlfAa-LN1SA for details). It's definitely not the default yet, but there absolutely is effort to use it for particle accelerators.

thesuperbigfrog 4y ago

>> What’s the story with Rust and verification nowadays? It is in progress but likely several years to go before a MVP is released. Ferrocene [1] is the primary effort that I am aware of and that seems to be making progress towards a verified rustc suitable for safety critical work. Ferrous Systems is working with AdaCore and just released the Ferrocene Language Specification [2] to formally document the Rust subset that Ferrocene will use. [1] https://ferrous-systems.com/ferrocene/ https://ferrous-systems.com/ferrocene/ [2] https://ferrous-systems.com/blog/ferrocene-language-specification/ https://ferrous-systems.com/blog/ferrocene-language-specific...

deleted 4y ago

[deleted]