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

• electrolysis

  2 322 10.0 Lean

  Simple verification of Rust programs via functional purification in Lean 2(!)

How do you represent this?

However, this insight holds for relatively common forms of ownership, and you can see this exploited in electrolysis: https://github.com/Kha/electrolysis

• winnow

  8 397 9.6 Rust

  Making parsing a breeze

  

I feel like I'll have to read up some more to have the background to fully understand the article but one thing I wanted to point out is a difference between `fn rand_int(rand: &mut Random) -> i64` and `fn rand_int(ran: Random) -> (i64, Random)`, at least in Rust. With the version that moves `Random`, the return type is bigger and may spill over from registers to the stack which may cause a significant slow down, more than the code of Vale's generation check, I suspect.

I've run into this with my parser combinator library, winnow [0], and am considering switching from the nicer functional model of moving to the more imperative model of `&mut` [1].

[0]: https://docs.rs/winnow/latest/winnow/

[1]: https://github.com/winnow-rs/winnow/issues/72

• WorkOS

  workos.com sponsored

  The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.

  

Suggest a related project