3 ms·
While Ada is a great and sadly underused language, if my memory serves, it's not out-of-the-box memory-safe by today's definitions. I seem to recall that it tak
by Yoric 11mo ago
While Ada is a great and sadly underused language, if my memory serves, it's not out-of-the-box memory-safe by today's definitions. I seem to recall that it takes Spark to make it memory-safe.
- themafia 11mo ago> by today's definitions. What are todoay's definitions? If Ada simply had more thorough rules but introduced an "unsafe {}" construct, then what would the practical difference actually be? Compiler defaults?
- RavSS 11mo agoSPARK is practically just a restricted version of Ada with a few added features for formal verification. You can write a program primarily in SPARK but disable said restrictions based on circumstance by setting the `SPARK_Mode` pragma/aspect to `off` on a package, procedure, function, etc. Mixing Ada and SPARK is trivial. I guess it is similar to Rust code that uses `unsafe {}` as the other poster mentioned (maybe `unsafe fn` for a closer analogy). My knowledge of Ada/SPARK is much greater than what I know about Rust, so I might be guessing wrong.
- Measter 11mo agoSo in Rust an unsafe block and an unsafe function mean two different things. An unsafe block allows you to do things that are unsafe, such as dereference raw pointers, access union fields, calling unsafe functions, etc. Unsafe functions mark that the caller is responsible for upholding the invariants necessary to avoid UB. In the 2021 and earlier editions, they also implicitly created an unsafe block in the body, but don't in 2024. Or, in a more pithy tone: an unsafe block is the "hold my beer" block, while an unsafe function is a "put down your beer" function.
- pjmlp 11mo agoSPARK is like Ada's version of Rust's clippy.
- GhosT078 11mo agoI disagree. SPARK is all about using formal methods to statically prove software properties. Clippy seems more comparable to parts of AdaCore's other static analysis toolset (gnatsas). See https://docs.adacore.com/live/wave/gnatsas/html/user_guide/faq.html#what-is-the-difference-between-gnat-sas-and-spark https://docs.adacore.com/live/wave/gnatsas/html/user_guide/f...
- pjmlp 11mo agoI know SPARK capabilities, the point was more that Rust also isn't without extra help to enforce specific coding practices.