is there any language like Rust, with a similar notion of lifetimes and references, and deterministic memory management?

@sodiboo i don't really know it at all, but _possibly_ ObjC/Swift ARC?

it's not really the same, and this space is generally _quite_ sparse

@r Swift has a lot of similarities with Rust and definitely does deterministic memory management, but it does NOT have the primary trait i was asking about: “lifetimes and references”. Swift does not at all support any notion of borrowing like Rust. To pass a “reference” into a function, it will have to be an owned reference counted handle, which is fine for most programs but definitely not at all the same thing as what Rust generally does.

@sodiboo ats, kinda?
you have linear types rather than affine types (stuff has to be consumed exaxtly once, rather than at most once, meaning you can have eg two different drop-like functions and the compiler ensures that you call one of them in all possible paths) and have explicit proofs for stuff (for example "there is memory at this address" and "this memory has been initialized"; they behave a bit like zero size types and are often used similarly to state types in rust)

@sodiboo main differences:
compiles to C and especially for lower level stuff relies on having at least some C that you wrap properly, and is over all more focused on the embedded proof assistant, which gives a lot of flexibility

also a pain in the ass to use, especially if you're trying to read one of the error messages
also "viewt@ype" as a linear viewtype, because that's obviously where the @ goes

@sodiboo in general the stdlib has a bunch of crazy naming conventions that never get explained (this is more or less just some profs pet project, even though ats3 is ready for enterprise by definition (too lazy to find the quote))

@sodiboo i've no idea^^
definitely not ats

@sodiboo i think that is what you asked for

rust memory management is a combination of:
- affine types (let x = y; invalidates y), ats does this with the "used at most once" part of linear types' "exactly once"
- raii (aka drop) allowing you to make sure some code gets called on every code path, allowing stuff like reliable Rc, ats does this with the "at least once" part of linear types
- not allowing anyone else to borrow when there's a &mut, ats does this with weird proofs that no one else...

@sodiboo hit the character limit exactly where it was clear what i was saying anyways, so i won't finish my sentence

@sodiboo maybe English or Spanish

@Bosspaint hm. pronouns and other forms of indirect address do exist in a lot of natural languages. i can easily refer to a previous subject in a shorter way, and arguably, that is a “reference” with a “lifetime” because after a certain point, it is no longer valid and any competent speaker will generally “reborrow” the subject by naming it again.

but i don’t think this at all satisfies the requirement of “deterministic memory management”. because, obviously, there are no fixed rules to exactly when and how this works or doesn’t.
and, there is not exactly a compiler or linter that can catch mistakes before you say them. so, it’s as useful as saying that “yeah ! C has lifetimes and references ! you can’t reference a variable after it’s been freed, that’s Undefined Behaviour”. obviously, i mean a language where the compiler enforces these kinds of constraints authoritatively. natural languages are disqualified on that requirement alone. (and no, Académie Française does not count as a compiler, no matter how authoritative they want to be about French)

@sodiboo you made me look at ats code again
and i'm surprised i somehow was once able to understand what's going on
my instance does not give me the emoji to express the confusion and disgust looking at this syntax

@sodiboo right something with a nullable pointer
[l:agez] something(l)
vs something with a non-null pointer
[l:addr | l > null] something(l)

agez being a type alias meaning "address greater or equal to zero", on a non-negative type

@sodiboo hell yeah
have fun!

@sodiboo i also *strongly* recommend
1. ats-acc (https://github.com/sparverius/ats-acc/) for easier to read errors (sadly it hides info you need in some cases)
2. learning what PMVtmpltcstmat means, specifically that peeemveeteeempeeellteeseeessteeemmaytee not defined means you forgot to include the atspre_staload or whatever the file was called, which defined a macro that evaluates to NOTHING, but the compiler emits that :)

@sodiboo also try to guess what it stands for, it's a fun game

@sodiboo i'm not quite sure how "in a scope" that is
but it is very simple and practical :3

@sodiboo mhm! keeps most of the simplicity while only relying on features the language has anyways

haskell also does operators in a fairly similar fashion, where you can just
let (+) = something very cool
in 5 + 3

@sodiboo iirc in haskell an operator is just a function that has a non-alphanumerical name :3

@sodiboo substituting substitutions 🥴

@sodiboo it is a very unusual language in general^^

a lot of the weirder choices are justifiable by thinking about if hwxi took this from C or ML and specifically when something was mixxed

@buffet @sodiboo there's also F*/Low* (and Idris2, partially Haskell's broken LinearTypes, etc) for linear types and typed memory management
There's stuff based on separation logic if you wanna jump deeper in
One of these days I'll actually learn ATS as well

@tranquillity @sodiboo right i fully forgot about f*/low*
i ran into some issues when i looked into it forever ago, but i should try again!

@buffet @sodiboo the procedure for getting the toolchain working + the documentation are pain concentrate and nonexistent (in this order)

@sodiboo too tired to fully understand, but i think should be possible?
you *can* force something to be handled

@sodiboo yes, lots of edging in general, hwxi's really into that

@sodiboo hahahaha this is actually the function i was looking for when i looked at ats code the other day^^^

@sodiboo https://github.com/githwxi/ATS-Postiats/blob/5e752821de2af56eb1c62399ff7f552ba291ef64/doc/BOOK/INT2PROGINATS/CODE/CHAP_EFFECTFUL/permord.dats#L104

@sodiboo hurt people hurt people 😔

@sodiboo @buffet @nea89 I wanna watch this live, sodi learns ATS and Lean
Do Agda and Coq too plz
I'd also ask for Idris2 and F* but I already mentioned those before

@sodiboo yeah good luck

@sodiboo yup, this is great :3

@sodiboo uh probably best to look at compiler output

i'd assume it just puts everything in a c struct, which means you'd probably end up with padding after the pointer

@sodiboo why would it not be possible? different envs would compile to different structs in C i think

@sodiboo ah right
hm

@sodiboo i'm not sure i've ever used -<clo> tbh

@sodiboo i mean i assume that it's just gonna have padding to whatever the largest required alignment on on that machine is

@sodiboo proving something like x < 256 is so simple it's great
you'll love to see that in a later chapter of the book!

@sodiboo when you get an index from some iteration method, that also proves that you *can* access at that point (unsure how this'd look with mutation tbh) which means you can safely access there 👍

@sodiboo @nea89 @tranquillity not live enough! need more updates! straight to my brain!

@sodiboo check out ~ATH its a great language with uhh . lifetimes . yea

@sodiboo @buffet @nea89 yaiii

@sodiboo @buffet @nea89 (as an aside, Lean is not really used often for memory safety models & verifying low level code, is it? I at least haven't seen it done yet I mostly see F* and Coq for this (and ofc Isabelle ig))

@sodiboo @buffet @nea89 F* is used like this for eg. https://github.com/signalapp/SparsePostQuantumRatchet#formal-verification

@sodiboo i don't rember fully tbh

@sodiboo epic

@sodiboo can you send the error?

@sodiboo write a function that just eats it

@sodiboo like obviously don't, but

@sodiboo you fool! what i did i tell you about PMVtmpltcstmat when i introduced atc-acc?

internal compiler macro used to add template expansions or something that expands to nothing

you forgot some prelude header

@sodiboo yeah idk i never got this part of ats
in my mind this is in "this must never happen" territory along at least 3 axes

@sodiboo there's a reason i have PMVtmpltcstmat memorized all these years later

@sodiboo yeah it's defined somewhere, just get that 👍👍

@sodiboo uh i cannot, i forgor
i'll try to get it to compile when i'm on computer

@sodiboo i forgor

@sodiboo wait i'm confused, i remember this being a macro that takes a type and a value and returns the value or similar, but that wouldn't even work syntactically with the array index, would it?

@sodiboo uh so maybe this is the result of type params not being applied or resolved correctly, also the reason you get back a linear size_t is probably because {a:vt@ype}

@sodiboo i've no idea