mei on Nostr: nprofile1q…d6kk0 nprofile1q…lnalw This is something that I feel is commonly ...

nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysyd6kk0 (nprofile…6kk0) nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqh2h820tdg9kk8eufek4a3ajn9eld5pq77fha7kwezpzgsvhdm97sqlnalw (nprofile…nalw) This is something that I feel is commonly misunderstood about Rust by people outside the community: the whole point of Rust is that you can build sound abstractions on top of small amounts of unsafe code. This is the key tradeoff that Rust got right: if you insist that the compiler is able to verify absolutely everything, you either get extremely limited expressiveness, or introduce a lot of complexity for being able to prove arbitrary memory management patterns correct (see e.g. RefinedC and how they essentially need to pull in an entire proof assistant, or ATS which again, is itself a very obtuse proof assistant).

Rust found the perfect middle ground: lots of practical impact for correctness, with the effort required still being low enough to get massive adoption.