Home | Notifications | New Note | Local | Federated | Search | Logout

Note Detail

Reply to @icedquinn@blob.cat
Q.U.I.N.N.@icedquinn@blob.cat (2026-10-10 07:49:48)
@sun > https://github.com/bendlang/bend/blob/main/paper/BendTT.pdf

oh they're doing ATS' ghost code thing. linear typed proofs. very strong if they get it right. ATS' failure was it never got a syntax that was any good. writing it sucked shit, it was effectively unlearnable.

i mewed a time or two about something like term rewrites or constraint handling rules as the type system. goofy, but old and studied, and the strongest part of ATS proofs in general is they stop you from passing shit where it doesn't go. (ATS in particular can attach proofs to FFI boundaries; you can actually state that C code is misbehaved or assert its well behaved and bring the proofs back in.)

eh i'll read the rest of the paper
---Reply---
Blurry Moon@sun@shitposter.world (2026-10-10 07:52:00)
@icedquinn yeah I have heard good things about this