Verbose is a small experimental language I build — its compiler proves properties about your code (termination, sound types, declared effects) and emits tiny x86-64 machine code: no runtime, no GC, no libc. This post stands on its own.
Picture a 943-byte file. Smaller than a long text message. You run it and send this:
GET / HTTP/1.0
It answers:
HTTP/1.0 200 OK
Content-Length: 29
Hello from Verbose over HTTP!
No Node, no Python, no nginx in front. No runtime, no garbage collector, not even the C library. 943 bytes, alone against the network.
And that's not even the interesting part. That binary was written by a compiler which is itself written in Verbose — the one that, last month, reproduced itself byte for byte. The language no longer merely compiles itself: it now produces the kind of program people actually write.
Serving HTTP when you have nothing
The analogy first, before any jargon.
You open an office. To receive clients you need four things, in this order:
- Get a phone line installed. No number yet, just the handset.
- Get a number — 18893. Now people can reach you.
- Lift the handset and put it on the desk: you're reachable, calls can queue up.
- Take the calls, one at a time. Each one: listen, answer, hang up. Then take the next.
That is exactly what a server does, with four calls into the kernel:
socket() → "install me a line" → returns a file number (fd)
setsockopt() → "when I hang up, free the line (SO_REUSEADDR)
immediately, don't hold it
blocked for a minute"
bind(18893) → "my number is 18893, (INADDR_ANY = on every
on every line" network interface)
listen() → "handset off the hook: queue
incoming calls"
┌── loop, forever ──────────────────────────────────┐
│ accept() → take the next call │
│ (waits if there is none) │
│ read() → listen to what the client says │
│ write() → answer │
│ close() → hang up THIS call │
└──────────────── and start over ───────────────────┘
That's it. There is nothing else in an HTTP server. Everything you know — Express, Flask, Spring — is a comfort stack on top of those four lines. The comfort isn't useless, but it isn't necessary: that's why 943 bytes are enough.
The first slice (S1) does precisely that and no more: the handler returns a response written ahead of time, the same for everyone. It's the smallest object still deserving the name "server".
The pivot: reading what the client said
A server that always answers the same thing is an answering machine. To go further you must understand the request. That's slice S2 — the pivot of the whole arc: nothing after it exists without it.
The client sends a run of bytes. Raw. Two pieces of information have to be cut out of it:
What arrives on the wire (bytes):
G E T / h e l l o H T T P / 1 . 0 \r \n \r \n
└──┬──┘ ▲ └────┬────┘ ▲
│ │ │ │
│ space │ space
│ │
method path
What the parser extracts, into two "slots":
req.method → pointer to "GET" + length 3
req.path → pointer to "/hello" + length 6
One detail that matters: nothing is copied. We only note where it starts and how long it is. The bytes stay where the kernel dropped them. An address and a length — two numbers — not a string copied somewhere else.
Those two slots, req.method and req.path, are the raw material for everything that follows.
Answering differently per request
Slice S3: routing. Once you know what was asked, you can answer differently. Then S4: build the response body from the request.
Here is a real example from the repo (examples/echo_path.verbose), trimmed:
rule echo_handler
input:
req : HttpRequest
output:
resp : HttpResponse
logic:
resp = if req.method == "GET"
then HttpResponse { status: 200, body: concat("got GET on ", req.path) }
else if req.method == "POST"
then HttpResponse { status: 200, body: concat("got POST on ", req.path) }
else
HttpResponse { status: 404, body: concat("unsupported method ", req.method) }
proofs:
purity:
reads : [req.method, req.path]
service echo_server
listen:
protocol : http_1_0
port : 18893
max_request : 4096
handler: echo_handler
Walk one call through, concrete values at every step:
1. Client sends : "GET /hello HTTP/1.0\r\n\r\n"
2. Parser fills : req.method = "GET" req.path = "/hello"
3. Rule evaluates : req.method == "GET" → true, first branch
4. concat assembles : "got GET on " + "/hello" → "got GET on /hello"
5. Binary writes : HTTP/1.0 200 OK
Content-Length: 17
got GET on /hello
Note the proofs: block. It declares: this rule reads req.method and req.path, and nothing else. That's not a comment — the compiler checks it. If the logic read a third field without declaring it, it wouldn't compile. The language's standing promise: the author declares, the binary doesn't drift.
And the concat in step 4 deserves a note. Until S4, the response body had to be written ahead of time. From S4 on it is assembled at call time — and its buffer lives on the iteration's stack. The loop frees it in one instruction before the next call, whichever branch ran. No allocation, no deallocation to track, no possible leak.
The detail that lands: one log line, one syscall
Slices S5a and S5b: the server now writes its access log. And that's where the most instructive part hides.
A log block looks like this (real example, examples/audit_strict.verbose):
log:
append_file "/tmp/audit.jsonl"
concat("{\"method\":\"", req.method, "\",\"path\":\"", req.path, "\"}\n")
on_error: abort
The first implementation did the obvious thing: one write() per piece of the concat. Disassembling the compiled binary showed it plainly — four successive writes:
0x202 open ← open the file
0x217 write ← "{\"method\":\""
0x23a write ← "GET"
0x24c write ← "\",\"path\":\""
0x26f write ← "/hello\"}\n"
0x279 close ← close
It works. As long as there is exactly one client.
Now two requests arrive at once. The kernel may interleave their writes — it has no reason not to:
What you wanted:
{"method":"GET","path":"/hello"}
{"method":"POST","path":"/submit"}
What you can get:
{"method":"GET","{"method":"POST","path":"/hello"}
path":"/submit"}
Two corrupted lines. Neither is true. And it's the worst kind of bug: it doesn't show up in development (one client), it doesn't crash anything, it only appears under load now and then — and it damages precisely the file you read to understand what happened. An audit log that lies under load is worse than no log at all.
The fix (PR #138): replace the N writes with one writev. Same idea as an envelope. Instead of mailing four sheets separately and hoping they arrive in order, you put them all in one envelope and mail that. The postman can no longer shuffle them with the neighbour's.
BEFORE — 4 calls, interleavable AFTER — 1 call, atomic
write(fd, "{\"method\":\"", 11) iov[0] = ("{\"method\":\"", 11)
write(fd, "GET", 3) iov[1] = ("GET", 3)
write(fd, "\",\"path\":\"", 10) iov[2] = ("\",\"path\":\"", 10)
write(fd, "/hello\"}\n", 9) iov[3] = ("/hello\"}\n", 9)
writev(fd, iov, 4)
open → write → write → write → write open → writev → close
→ close
The iov array (four address + length pairs) is built on the stack, and syscall 20 consumes it in one go. All or nothing: the whole line is written, or none of it is. Never half.
It looks like an optimization detail. It is one — six syscalls down to three. But above all, it's a change of guarantee: the log file becomes a sequence of complete lines, by construction, under any concurrency. And it's the prerequisite for the next slice, on_error: abort — "if I can't write the audit trail, stop everything". That promise means nothing if a line can already come out cut in half.
What it means
The seven slices:
S1 a server that always answers the same → 943-byte ELF
S2 parse the request (method, path) → the pivot
S3 route on method and path
S4 build the body from the request
S5a write log lines
S5b logs containing request fields
5b.5 one line = one writev = atomic
In six days the self-hosted compiler went from "it can reproduce itself" to "it can produce a web service that parses, routes, answers and traces". Those are very different things. The first proves the language stands up; the second proves it's good for something.
And the limit, named as usual: v0.10.0 still isn't tagged. main is 54 commits ahead of v0.9.0 — the fixed point, the verifying bootstrap, the effects tier, and now the service arc. There's a release-shaped moment there, ripe for weeks. It's waiting on a decision, not on code.
943 bytes that answer HTTP. Written by a compiler that wrote itself. No runtime, no libc, and logs you can believe.
French original on arcker.org.
Top comments (0)