Build it in edda
Network services
A server is a program that holds authority over a socket and exercises it for strangers. Edda makes that authority a parameter, the handler's failure modes a row on its signature, and the response invariants contracts the build proves.
This page is the demo
The site you are reading is a verified edda program: an HTTP server over std.net.socket with the hermod codec, holding exactly four capabilities — a network, a read-only view of its own source tree, standard output, and an allocator. Its main signature declares all four; nothing else is reachable.
What the language gives a service
Narrowed capabilities
A handler that only reads templates gets a filesystem scoped to that directory, read-only. The narrowing is one-way and checked; a confused-deputy bug is a type error.
Errors on the row
Every way a request can fail — decode, allocation, socket — is an err: entry on the handler's effect row. Nothing is thrown past you; an unhandled case fails the build.
No orphaned work
Tasks live inside a scope that cannot exit while children run, and nothing mutable crosses a spawn boundary. Connection handling is structured or it does not compile.