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: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
---Reply---
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

---Replies---

Blurry Moon@sun@shitposter.world (2026-08-22 10:03:06)
@icedquinn no actual formal verification is happening at this stage, just added annotations to make it easier in the future. I don't know what I'm doing tbh