[HN Gopher] How Dada enables internal references
___________________________________________________________________
How Dada enables internal references
Author : vrnvu
Score : 21 points
Date : 2026-02-27 14:58 UTC (2 days ago)
(HTM) web link (smallcultfollowing.com)
(TXT) w3m dump (smallcultfollowing.com)
| nine_k wrote:
| This is interesting and somehow neat, but how sound is it?
|
| Lifetimes are based on affine types, which have some proven
| mathematics backing their properties. This is what guarantees the
| absence of invalid references, the fearless concurrency, etc.
|
| What is backing the place-based system, and what formally proves
| that it always works?
| brson wrote:
| Quite a lot of type system modeling has gone into Dada so far,
| though I don't know the details. Some of that work is here:
| https://github.com/dada-lang/dada-model
| jadengeller wrote:
| I think this is a bit similar to Mojo's origin types:
| https://docs.modular.com/mojo/manual/values/lifetimes/#origi...
| armchairhacker wrote:
| I believe places are a much better model than lifetimes, but
| there are challenges not discussed in this post. Ex: what would a
| linked list's definition and methods look like? How does Dada
| handle mutation and deallocation?
| amluto wrote:
| Can Dada put a value on the stack and pass any sort of mutable
| reference to it to a function? I don't know the syntax, but
| maybe: let x: given i32 = 42 f(x.mut)
| // now x == 43
|
| If all permission variants of a type are shallowly laid out like
| the raw type, then x and x.mut are literally 32-bit integers, so
| how does one mutate it from a function body? A special boxed i32?
___________________________________________________________________
(page generated 2026-03-01 23:01 UTC)