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

Note Detail

Reply to @icedquinn@blob.cat
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
---Reply---
Q.U.I.N.N.@icedquinn@blob.cat (2026-08-22 10:02:51)
@sun :blobcatpensive2: hoare and separation logic. that's not what makes something formally verifiable, but it helps.

---Replies---

Blurry Moon@sun@shitposter.world (2026-08-22 10:03:12)
@icedquinn yeah

Blurry Moon@sun@shitposter.world (2026-08-22 10:08:30)
@icedquinn yeah really trying to make sure its amenable to static analysis