|
The README clarification is useful, and I am happy to refine my original comment accordingly.
Calling the use of "unsafe" itself “cheating” was too broad. A freestanding kernel necessarily has operations at hardware, ABI, allocator, paging, interrupt, and raw-pointer boundaries that Rust’s type system cannot prove safe. Rust’s own terminology is that an "unsafe" block discharges a proof obligation which the compiler cannot check; it does not mean that the code is automatically defective.
That said, counting and locating "unsafe" was not an “arbitrary” or irrelevant search. It identifies the portions of a supposedly memory-safe kernel that belong to its trusted computing base and therefore merit closer review. The repository itself makes exactly this distinction: it says that "unsafe" is concentrated at the hardware boundary and in intrusive data structures, with explicit safety contracts. That is a substantive and reassuring answer to the concern—not evidence that asking about the concern was illegitimate.
The technically appropriate next questions would be whether those contracts are complete, whether the safe abstractions actually preserve them, and whether tools such as Miri, sanitizers, model checking, fuzzing, or formal verification can cover some of the remaining obligations. Boot tests and emulator differential testing provide valuable evidence, but they are not general proofs of memory soundness.
So, to be precise: nanokrnl is an impressive proof of concept, and its use of localized, documented "unsafe" is normal for kernel development. It is also correct that Rust cannot by itself guarantee the soundness of those regions. Both statements can be true simultaneously.
What is not productive is repeatedly substituting speculation about my motives, unrelated accusations about another repository, or demands that a forum observation arrive with a completed patch. Your accusation about proprietary SDK code was already shown to be false. I have now clarified my wording and the technical issue. Unless you have identified a specific error in the analysis or a specific unsound block in the code, there is nothing further to argue about. Please let the thread return to the project itself.
|