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

Note Detail

Reply to @icedquinn@blob.cat
Blurry Moon@sun@shitposter.world (2026-08-22 09:52:41)
@icedquinn I needed a pascal-like capability language that had a narrow formal verifiable subset
---Reply---
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 09:54:42)
@sun idk what that means. pony types?

formal verification has many names underneath.

---Replies---

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"

Blurry Moon@sun@shitposter.world (2026-08-22 10:01:08)
@icedquinn really simple, set of annotations to state valid inputs and outputs, expected outcome of loop operations