Borrow Checking, RC, GC, and Eleven Other Memory Safety Approaches

The borrow checker is only one component of the means by which Rust statically enforces thread safety. If you design a language that doesn't allow pointers to be shared across threads at all, then you wouldn't need a borrow checker. Likewise if you have an immutable-only language. What's interesting about Rust is that it actually supports this safely, which is still unbelievable sometimes (like being able to send references to the stack to other threads via std::thread::scoped).

> Interaction nets are a very fast way to manage purely immutable data without garbage collection or reference counting.[...] HVM starts with affine types (like move-only programming), but then adds an extremely efficient lazy .clone() primitive, so it can strategically clone objects instead of referencing them.

This is wrong, Interaction nets (and combinators) can model any kind of computational systems, including ones that use mutation. In fact, ICs are not really about types at all, although they do come from a generalization of Girard's proofs nets, which came from work in linear logic.

The interesting thing about ICs is that they are beta-optimal (any encoding of a computation will be done in the minimum number of steps required -- there is no useless work being done), and maximum-parallel with only local synchonization (all reduction steps are local, and all work that can be parallelized will be parallelized).

Additionally ICs have the property that any encoding of a different computational system in ICs will preserve the asymptotic behavior of all programs written for the encoded computational system. In fact, ICs are the only computational system with this property.

Interaction nets absolutely require garbage collection in the general sense. However, interaction combinators are linear and all garbage collection is explicit (but still exists). HVMs innovation is that by restricting the class of programs encoded in the ICs you can get very cheap lambda duplication and eschew the need for complex garbage collection while also reducing the overhead of implementing ICs on regular CPUs (no croissants or brackets, see Asperti[1] for what that means).

Having a linear language with the above restriction allows for a very efficient implementation with a very simple GC, while maximizing the benefits of ICs. In principle any language can be implemented on top of ICs, but to get most benefits you want a language with these properties. It's not that HVM starts with affine types and an efficient lazy clone operation, it's that a linear language allows extremely efficient lazy cloning (including lambda cloning) to be implemented on top of ICs, and the result of that is HVM.

> The HVM runtime implements this for Haskell.

This is very wrong. HVM has nothing to do with Haskell. HVM3 is written in C[2], HVM2 has three implementations, one in C[3], one in Rust[4], and a CUDA[5] one. HVM1 was just a prototype and was written in Rust[6].

HOC[7], the company behing HVM provides two languages that compile to HVM, Bend[8], and Kind[9]. Bend is a usual functional language, while Kind is a theorem prover based on self types.

Haskell is not involved in any of these things except that the HVM compiler (not runtime) is written in Haskell, but that is irrelevant, before Haskell it used to be written in TypeScript and then in Agda (Twitter discussion, sorry, no reference). It's an implementation detail, it's not something the user sees.

Please note that HVM adds some stuff on top of ICs that makes it not strictly beta-optimal, but nevertheless the stuff added is useful in practice and the practical downgrade from theoretical behaviour is minimal.

[1] Andrea Asperti, The Optimal Implementation of Functional Programming Languages, ISBN-13: 978-0060815424

[2] https://github.com/HigherOrderCO/HVM3/blob/main/src/HVML/Run...

[3] https://github.com/HigherOrderCO/HVM/blob/main/src/hvm.c

[4] https://github.com/HigherOrderCO/HVM/blob/main/src/hvm.rs

[5] https://github.com/HigherOrderCO/HVM/blob/main/src/hvm.cu

[6] https://github.com/HigherOrderCO/HVM1

[7] https://higherorderco.com

[8] https://github.com/HigherOrderCO/bend

[9] https://github.com/HigherOrderCO/kind

Side notes are a great layout for most deeper reads.

There's some great tooling for that via https://edwardtufte.github.io/tufte-css/ and https://tufte-latex.github.io/tufte-latex/.

> that other systems don't have this assurance

My understanding is that most (all?) GC languages are memory safe, but do not ensure statically verifiable thread safety at all. Like Java, Go, C#, Python, etc.

The way you make garbage collection deterministic is not by doing regions but by making it concurrent. That’s increasingly common, though fully concurrent GCs are not as common as “sorta concurrent” ones because there is a throughput hit to going fully concurrent (albeit probably a smaller one than if you partitioned your heap as the article suggests).

Also, no point in calling it “tracing garbage collection”. Its just “garbage collection”. If you’re garbage collecting, you’re tracing.