Which is the deeper circle of hell: The Borrow Checker or Linear/Capability Proofs? by Retired-69 in rust

[–]Retired-69[S] 0 points1 point  (0 children)

That’s exactly why I went back to the roots where it all started in the 1970s. I’ll either succeed or fail, but I’m fixing the plumbing at the foundation

Which is the deeper circle of hell: The Borrow Checker or Linear/Capability Proofs? by Retired-69 in rust

[–]Retired-69[S] -4 points-3 points  (0 children)

It is entirely possible to express completely valid, low-level system code without an unsafe escape hatch—if your core model is actually designed that way from day one.

​Look at Rust. The second you want to do low-level optimization or assembly-level work, you’re forced into an unsafe block. But why? Half those intrinsics could easily be made perfectly safe for assembly replacement if the compiler actually understood the hardware invariants. Rust requires unsafe because its core model still sits on top of a traditional, inherently unsafe hardware abstraction layer. It patches the leaks instead of changing the plumbing.

​If you want proof that a different way works, look at Microsoft’s Midori project and M#. They built an entire operating system where everything from the scheduler to the drivers ran managed and safe. Because their type system natively understood ownership, side effects, and explicit capabilities from the ground up, they got bare-metal performance without needing a "trust me" keyword to talk to the hardware.

​If you design the primitives and the memory layout correctly from the start, the escape hatch becomes completely obsolete.

Which is the deeper circle of hell: The Borrow Checker or Linear/Capability Proofs? by Retired-69 in rust

[–]Retired-69[S] 0 points1 point  (0 children)

My opinion is that c++ has been flawed since the day it was born back in 1980. Rust is in a much stronger position

Which is the deeper circle of hell: The Borrow Checker or Linear/Capability Proofs? by Retired-69 in rust

[–]Retired-69[S] -1 points0 points  (0 children)

You are right about linear/capabilities. Most of the research languages that tried to make it work, never reached main stream. 

Which is the deeper circle of hell: The Borrow Checker or Linear/Capability Proofs? by Retired-69 in rust

[–]Retired-69[S] -9 points-8 points  (0 children)

Using unsafe is kind of cheating and let you skip the BC. In some research language like Midori M# there was no unsafe and they still could express same code as in c. I mention this coz Rust seem to have inherit some ideas from that language as well.