3 ms·
> it a bit too idealistic and not pragmatic enough This is an ideal programming language for certain types of people. It also gives the programming language ce
by LoganDark 1y ago
> it a bit too idealistic and not pragmatic enough
This is an ideal programming language for certain types of people. It also gives the programming language certain properties that make it useful when provable correctness is a concern (see Ferrocene).
- AlotOfReading 1y agoLast time I talked to the ferrocene people they had no plans to do anything with formal methods. Has their scope expanded?
- _flux 1y agoMaybe it was intended to refer to RustBelt. I haven't been following their work, though. It seems they are working on stacked borrows.
- steveklabnik 1y ago> I haven't been following their work, though. It seems they are working on stacked borrows. We're a few years past that, there's now 'tree borrows' which just had its paper published: https://www.ralfj.de/blog/2025/07/07/tree-borrows-paper.html https://www.ralfj.de/blog/2025/07/07/tree-borrows-paper.html
- LoganDark 1y agoSorry, I didn't mean provable correctness as in using formal methods, I meant it in terms of far stronger compiler guarantees about especially things such as memory safety. I also personally find Rust code far more pleasant to write and to reason about compared to C/C++ because of how well-defined and consistent it is.