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

Note Detail

Reply to @sun@shitposter.world
Blurry Moon@sun@shitposter.world (2026-10-08 13:18:58)
@demha @lain @mischievoustomato to add a little more clarity here, there are certain things that can be mechanically tested and proved, like using strict typescript typing, and build-time checks that certain types have certain annotations. so, that at least proves intent. then, there are things you can't easily prove mechanically. So, I instructed the LLM: never change a function against it contract; never change the contract to make a function do something I asked. only permit an explicit request to change the contract first, then a second request to implement the change. and, the annotations are the source of truth for correctness audits.

it's not foolproof. but it helps, a lot.
---Reply---
Tshering dempa@demha@comp.lain.la (2026-10-08 19:35:11)
@sun @lain @mischievoustomato i heard something about the bend language doing something like that with its LAWS.bend feature

---Replies---

Blurry Moon@sun@shitposter.world (2026-10-09 08:19:02)
@demha @lain @mischievoustomato very interesting.

so yeah, the huge problem is typescript doesn't have enough stuff to prove no side effects. best you can do is mitigate