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

Note Detail

Reply to @sun@shitposter.world
🌈ᚩ🌈@bonifartius@noauthority.social (2026-09-21 19:53:49)
@sun @waltercool @newt i'm not smart, i only fiddled with agda2 once for uni (failed horribly at that ;). it was interesting, but more because of the emacs environment which was actually pretty neat.
---Reply---
🌈ᚩ🌈@bonifartius@noauthority.social (2026-09-21 20:50:17)
@sun @waltercool @newt iirc provers are good for some things, like designing robust network protocols. 

for "real" programming you have to deal with the dirtiness of the physical world where things fail, so the interesting part is to find good ways to handle failure mode which work, in the real world.

---Replies---

Blurry Moon@sun@shitposter.world (2026-09-21 21:03:11)
@bonifartius @waltercool @newt looking at lean and koka. maybe it can be good for parts of an OS rammed through the C ABI