What Vale Taught Me About Linear Types, Borrowing, and Memory Safety

[bakul]

I certainly don't mean to make a "case for Rust" (or Vale) but I thought this might provide some insight into Rust's borrow checker etc. Perhaps understanding *why* Rust has these features might make us appreciate them and may be even help us figure out how to provide something similar in other languages.

What Vale Taught Me About Linear Types, Borrowing, and Memory Safety

[edit: recommend the following video if you are interested in linear types etc.]

View: https://www.youtube.com/watch?v=UavYVf0UEoc

 

[blackbird9]

https://vale.dev/

Not another one...

 

[Jose]

Linear types are so easy to understand! I may have to try to write some Vale to see if they're as useful as they seem.

 

[blackbird9]

Yeah, I was just reacting to the plethora of new programming languagues hitting the streets...

 

[Jose]

I feel ya. I've got fadlang fatigue too, but this one is actually interesting.

 

[mer]

Some of these new languages, are they simply "compilers enforcing correctness"? We all know the difficulty of enforcing correctness in C/C++ but are these new languages jus enforcing things via compilers?
If one actually pays attention to warnings from a C/C++ compiler, I think that covers quite a bit of correctness.

 

[Jose]

...languages jus enforcing things via compilers?

The Vale example is a compile-time check that raises an error: https://verdagon.dev/blog/higher-raii-7drl#a-real-world-example

If one actually pays attention to warnings from a C/C++ compiler, I think that covers quite a bit of correctness.

I spent some time at work this week wading through hundreds of compiler warnings, looking for the actual compilation error... Lesson learned: set your compiler's flags to treat warning as errors when you start your project. Any time later is almost certainly too late.

 

[zzfs6]

I think that linear types are a pretty neat idea. I think its a bit much to have a whole language built around them but it would be interesting to hack it into C, kind of like this implementation.

 

[bakul]

Here’s my simple minded explanation of Rust’s borrow checking: You can have any number of immutable references to an object (none of them are allowed to change any part of the object) or *one* mutable reference that can change the object. Either many immutable refs or one mutable ref but *never* at the same time. Most such uses can be checked by static analysis.

 

[zzfs6]

I wrote a simple implementation of linear types in C here. Feel free to try it out! It's pretty spartan at the moment but I'm planning on binding each Linear to a counter so it is actually correct.