A pair of Rust kernel modules
A pair of Rust kernel modules
Posted Sep 15, 2022 19:10 UTC (Thu) by Cyberax (✭ supporter ✭, #52523)In reply to: A pair of Rust kernel modules by Fabien_C
Parent article: A pair of Rust kernel modules
> Using Ada's formal verification subset (SPARK)
SPARK doesn't support dynamically allocated objects well: https://docs.adacore.com/spark2014-docs/html/ug/en/source...
It's similar to Rust without lifetime annotations and with less static analysis for stack objects.
There are academic papers that try to fix that, but the outcome would basically look like Rust.