Quote:
Originally Posted by WhoCares
The author puts some notes there:
Modern & safe by construction. unsafe is concentrated at the hardware boundary and in the intrusive data structures, each block with an explicit safety contract. SpinLock<T> owns its data and raises IRQL by construction, so the classic "touched shared state below DISPATCH_LEVEL" driver bug doesn't compile. Box/Vec/String work in-kernel and draw from NonPagedPool with the 'Rust' tag.
|
Thanks @WhoCares for pointing this out.
Yes, this is
exactly one of the
main reasons why I was trying to point out to @chants that he is unnecessarily trying to point out the not-so-relevant-in-practice code as "unsafe" through a cursory and arbitrary keyword search for "unsafe code".
The
nanokrnl project is definitely a ground-breaking project for those who understand the implications.
I would not have minded if chants provided some actionable code instead of just this statement:
Quote:
|
there should be some sort of formal proof/verification metadata extension for Rust that allows unsafe regions to be proven safe. Otherwise I consider these to be "cheating"
|
Peace
