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

Note Detail

Reply to @icedquinn@blob.cat
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
---Reply---
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 10:27:15)
@sun idk the short answer is read as much of why3 and agda/idris/lean/coq as you can stomach and go from there. lean might be the easiest because they actually want to ship product, so there's docs aimed at programmers. those are proofs through functions. souffle is used for a lot of analytics in some spheres, which is basically a huge datalog engine where you "compile" the program to a fact base and then write queries about it.

the most accessible weapons are why3 and souffle, in that you're dumping the program out to a different imperative language (whyml) or dumping the somewhat compiled IR in to facts (souffle) and then writing claims about it.

the lightweight weapons are reasoning about what the heavier weapons can prove and finding a way to make the failure states inexpressible without them. pony doesn't need theorem provers because he already proved the type system cannot express the failure states pony is intended to prevent, so it can get by much more cheaply by just committing to that type system.

this is ultimately why some languages get mad about stuff like pointer arithmetic. if you can do arbitrary pointering, you can no longer make static guarantees about points-to. (points-to analysis is a big deal in verification, there's specific optimizations in datalog literature to cope with the sheer number of pointers and their potential pointer locations.) some of the aircraft (where verification thrives) rules don't allow closure magic at all because its difficult/implausible to present a fully static CFG for them. (continuation passing has no implicit guarantee that code will ever resume in any meaningful way, although its possible to make them do so)

(the lightweight version also tends to shape the language and is inflexible, sadly, so unlike ATS you can't come back in the future and alter the axioms for a specific project.)

---Replies---

Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 10:30:48)
@sun i will now stop talking about this :gutkato_zipita: