5 ms·
That is true, but SPARK is more heavyweight and less mature than Rust. If someone wants to make the case that SPARK would be a better approach than Rust to wri
by roca 7y ago
That is true, but SPARK is more heavyweight and less mature than Rust.
If someone wants to make the case that SPARK would be a better approach than Rust to writing safe code in the Linux kernel, they should go ahead, but I haven't seen anyone make that case.
- pjmlp 7y agoHow is SPARK less mature than Rust given its use in the industry?
- roca 7y agoI'm talking about SPARK-with-pointers. As of June this year, that was still only available as a preview: > If you now feel like using them, a preview is available in the community 2019 edition of GNAT+SPARK.
- pjmlp 7y agoFair enough, however SPARK-without-pointers is even more constrained in what concerns dynamic allocation, basically it is forbidden and everything must be known at compile time.
- roca 7y agoThis shifting-the-referent bug annoys me, because it happens with C++ too. "C++ is really mature and there are so many C++ projects and developers!" "Yeah but it has these problems..." "Just use C++17, it solves all that!" ... but C++17 is not the language that is really mature and that all those C++ projects and developers are using.
- ajxs 7y agoI don't think anyone is going to make that case, given how lukewarm the response has been in the past, and how lukewarm the response to Rust is now. SPARK is used extensively in areas much more mission critical than the Linux kernel. One recent area I found it used which is very interesting is in the CoreBoot BIOS firmware. I'd hesitate to call SPARK a heavier language, but I'm not sure that's what you're saying. It's definitely far, far more mature than Rust.