Hacker Newsnew | past | comments | ask | show | jobs | submitlogin
Type Systems for Memory Safety (borretti.me)
6 points by ibobev on July 23, 2023 | hide | past | favorite | 1 comment


Amazing article! I especially like the distinction between resource safety and memory safety. I think a lot of folks don't realize that a memory safety approach can help or hurt one's resource safety.

The only mainstream language today that really nails resource safety IMO is C++. Ironically, Rust takes a bit of a step backward on this dimension, e.g. an AVL tree will likely need to be backed by a Vec and be more prone to "leaking" nodes, since the Vec owns the node, not the parent. Now imagine a program has actual resources instead of an AVL tree having nodes, and one can see the problem. A logical owner often needs to give up ownership to the central collection, losing resource safety.

That could be fixed by blending borrowing with linear types just like Austral did. [0] The logical owner (parent in AVL tree example) could wrap the child ID in a linear type, and thus can't accidentally drop() it, and must consume it by removing its referred node. I sometimes call this pattern of linear types "Higher RAII" [1].

> [Regions] do not address concurrency and data race freedom.

This is true of today's languages, but I hope to soon have a prototype of immutably borrowing an entire region at once to allow multiple threads to access it without data races.

[0] https://austral-lang.org/linear-types

[1] https://verdagon.dev/blog/higher-raii-7drl (am author)




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: