-
-
Notifications
You must be signed in to change notification settings - Fork 0
Developers
Your Name edited this page Jan 26, 2026
·
1 revision
proven gives you safety functions you can rely on, across many languages, with correctness proven in Idris 2.
What to know:
- All safety logic lives in Idris.
- Zig is a pure ABI bridge.
- Your language binding is a thin wrapper.
Usage model:
- Call binding function
- Zig ABI forwards to Idris
- Idris returns a proven result
If you see non‑Idris logic in a binding, treat it as unsafe and report it.