The Inevitability of the Borrow Checker
9 comments
·February 6, 2025pjc50
YorickPeterse
In Inko a borrow is sort of a hybrid in that it does increment a counter, but there's no shared ownership like there is in traditional reference counting (e.g. a borrow is never tasked with cleaning up data).
Terminology is a bit annoying here, as e.g. "reference" can also be interpreted as "a pointer", though it depends on who you ask. I stuck with "borrow" because that just made the most sense to me :)
agentultra
A nicely written article! And an interesting project.
Myself, I'd lean towards a sound (linear) type theory. If it's not too much trouble, insert the run-time checks in debug builds but use the type system to erase them for optimized builds. It might seem like the mountain is impossible to climb if you're not used to formalizing such systems but every mountain is surmounted one step at a time.
It's hard to bolt-on correctness after the fact. In my experience, for critical pieces like this, it's better to get the specification right first before digging in too deep and writing code.
Best of luck on the project either way you go. Memory safety is increasingly important!
YorickPeterse
Although linear typing is certainly interesting, I think linear typing on its own is not enough. That is, you basically end up with something like Austral where you use linear types _plus_ some form of compile-time borrow checking, at which point we're back at borrow checking (did I mention it seems inevitable?) :)
etyp
I like how this is structured. When I read that inline types get copied-on-borrow I was pretty put off. Then since fields of inline types can't be assigned new values it seems a bit better, as long as you roughly know what's happening. Hopefully the diagnostics are good enough there. I like the detailed alternatives that weren't chosen.
I appreciate being able to choose which side of the tradeoff (always-copy or heap allocated) you want to be on, but either way be assured it's safe. Not sure how I feel about it in practice without trying it, though :)
YorickPeterse
On the diagnostics side of things, the compiler produces these in two places:
1. If you try to define a `mut` field (= one you can normally assign a new value), it will produce an error at the definition site
2. If you try to do something like `some_inline_value.field = value` it also produces an error at the call/assignment site
The actual messages could use some improvements, but that's not a super high priority for the time being as I'm more focusing on the language overall.
null
ej1
This is a test comment posted using Playwright!
isoprophlex
Your bot can go fuck itself, the internet is zombiefied by undead AIs enough as it is.
This article seems to use "borrow" to mean what I would normally understand to be the reference count of a refcount-gc system? Rather than a Rust borrow, which is part of the type system and not counted at runtime.
In C# you can force a type to be stack allocated with "ref struct". https://learn.microsoft.com/en-us/dotnet/csharp/language-ref...