Claude Fable 5 wrote a booting, NT-shaped Rust kernel in 38 minutes

[chants]

Very cool. In terms of safety, I do see 53 .rs files with "unsafe": https://github.com/search?q=repo%3Am...pe=code&l=Rust

So it seems safety guarantees are still not assured - 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"

[Ibrahim_Mihai]

Originally Posted by chants

Very cool. In terms of safety, I do see 53 .rs files with "unsafe": https://github.com/search?q=repo%3Am...pe=code&l=Rust

So it seems safety guarantees are still not assured - 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"

Cheating? Look who's talking!

Well, there is still the same "unsafe code" issue with the vibe-coded decompilers you posted last week:
https://forum.exetools.com/showthread.php?t=21666
This is always a problem with vibe-coded content.

OTOH, at least the nanokrnl above is a excellent proof-of-concept of something that was only a pipe dream for many years.
If you've actually read the whole article carefully, you can see that it was meant only as a PoC and not for production use anyway!

A nano Windows kernel booting through a hand-built emulator in the browser, on its own NT syscalls, is quite an achievement.

Kudos to the creators of the nanokrnl projext!

[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.

Originally Posted by chants

Very cool. In terms of safety, I do see 53 .rs files with "unsafe": https://github.com/search?q=repo%3Am...pe=code&l=Rust

So it seems safety guarantees are still not assured - 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"

[Ibrahim_Mihai]

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:

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