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

Note Detail

Reply to @sun@shitposter.world
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 10:10:05)
@sun it largely means that you can make proofs about particular concerns. there are many ways to get there.

hoare logic is all about pre/post conditions, separation logic is basically that with some extra operators about splitting up a heap. they are ways to relate programs to formal logic.

HOL is sort of the easier formal logic since the kernel is just "true because we said so" and a couple of "true if these other facts were true." isabelle/hol has the sledgehammer which auto-derives a lot of proofs by SAT solving.

dependent types are basically turing complete macros, so they are cursed. i don't quite know how lean and coq deal with them; i think there's a proof layer and the code layer and they mix in some sideways means. ATS the proof is a value, it just doesn't exist at runtime, so some parameters exist at runtime and some don't, but it makes it neat and explicit.

what pre/post conditions do is basically let you outsource some proofs to why3. you write a compiler backend that spits out WhyML code and let Why3 outsource the checks to Z3 et all. this works great for some stuff (linear ranges and set memberships.) it can fall back to coq proofs for gnarly shit.

there's also souffle, but eh
---Reply---
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 10:14:48)
@sun i have some notes on "scriptable types" which was basically me just asking can we have discount dependent types as machinery without the appeal to hypothetical perfection.

nelua shows that letting you write to the AST is neat (not just "create code via macro" but they were lua tables, so macros could stash metadata in there for other macros.) ATS has two "universes" for ghost code and compiled code. (why3 and dafny call it "ghost code," because its a ghost, it exists to prove things to the compiler but it doesn't make it to execution.) so we could simplify it to 'ghost {...} runs ghost code' and 'ghost types are ghost code', and type checks just become 'run some code in the compiler's VM'.

nelua already does this with concepts; a concept is AST fed to a function which returns true or false. useful for metaprogramming, but instead of generating code we're vetting it.

its an interesting line of notes because it means you can get the core value of dependent types for much cheaper than people usually pay, though you have to bring the rigor separately

---Replies---

Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 10:15:38)
@sun i don't think this is a downside because logic systems always live with the ability to "prove false" with bad axioms, so "bring your favorite logic layer" isn't adding any more danger than already existed. it's just making dependent types a dime store implementation instead of intellectual masturbation