|
|
|
|
|
|
by c-cube
1318 days ago
|
|
|
Who said anything about RAII? Having RAII doesn't make C++ memory safe. If you can take a reference or pointer to some RAII-created vector, and access it after the vector is gone… then you're not memory safe? Yes, SPARK exists, and is very cool. I think there's work on a similar system for rust (or ferrocene, anyway, which is being co-developed by AdaCore: https://blog.adacore.com/adacore-and-ferrous-systems-joining...). It also seems that SPARK now has memory ownership and aliasing support, but only since ~2019 (https://blog.adacore.com/using-pointers-in-spark), and with clear inspiration from rust. It seems to me that this addition to SPARK was felt necessary by the AdaCore people, meaning that rust had something Ada did not support (or did not support well). |
|
|