[jblow]

> that lets the compiler apply its memory safety checks to all the places that call it

My point is that those memory safety checks are now meaningless.

> This is still a meaningful improvement to memory safety over C.

No, it really isn't. What you are describing is almost exactly what you get in C.

[howinteresting]

They are the opposite of meaningless. This is just straight-up incorrect, both in theory and in practice.

Please take some time and think about this a bit more. Please think about how code review processes work, how audits work, how human attention spans work. Please think about how people endlessly nitpick small PRs but accept large ones with few comments. What unsafe does is make it easy to spot the small bits of critical code to nitpick while not having to worry about safety for the rest.

You're better than this, Jon.

[Rusky]

They're conditionally meaningful: if a small amount of your program is correct, the entire program satisfies some useful properties.

This may or may not be something you care about, but it is certainly a meaningful tool that is quite useful to me, including when I use your type (3) style described in the sibling thread.

[lfairy]

So you're saying that Haskell's memory safety is meaningless too, because parts of its stdlib and runtime are written in C?