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 09:59:41)
@sun pony claims to have capability types. i guess that's what it has, though i don't see them called that elsewhere. viper has fractional types (values have shareholders, only the 100% shareholder can mutate, but you can allot out shares and each slot is now read-only until merged.) Isabelle does higher order logic (HOL) which is basically predicate logic kernel where you have a tiny set of privileged operations that produce axioms and facts and then further facts have to be derived. Agda/Idris/Lean/Coq have dependent types under some curry-howard thing. ATS does the curry-howard thing, but then proofs are themselves ghost code which have linear types (must be used exactly once.)

austral does linear types and its how i initially learned about them. 

ATS i think gets this the most intellectually correct, because proofs are threaded through the code. you don't prove some functional copy of the program does things, you state proof requirements at the call sites and provide proofs like they were data. which makes it tenable to carry proofs in imperative code, as ATS is basically "C with dependent types and god's shittiest ML dialect syntax"
---Reply---
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 10:01:21)
@sun i don't think you need any of the above to qualify as formally verifiable, either. it just means a static analyzer can make guarantees. some of the restrictions in aviation code are because those particular things are both good at hard real-time and also obvious to reason about (type pools in ada mirror how hard real timers actually reason about code) and static dispatch tables have every jump target known at build time

---Replies---

Blurry Moon@sun@shitposter.world (2026-08-22 10:02:38)
@icedquinn my main constraints for this language were: typed capabilities; amenable to future simple formal verification; simple implementation