HN user

mbrock

8,037 karma
Posts8
Comments2,494
View on HN

The same basically holds for proofs in the absence of coherent global correctness criteria like, say, confluence and normalization for a lambda calculus, or soundness and completeness for a logic.

Fable's napkin estimate of the effort required to produce a passable reference semantics for Postgres, which would involve novel discoveries in denotational semantics of concurrent transactions and so on, might be in the ballpark of 30–60 years of PhD level work.

So realistically I think the only way to validate a Postgres implementation involves differential testing, fuzzing, acceptance test suites, etc. And still you'll have bugs that need to be hammered out the good old fashioned way.

Faster in what browser, by what measure, for what modules? "X is faster than Y" without any concretization is usually meaningless.

You can do something like

       (y > 0 && x > INT_MAX - y) 
    || (y < 0 && x < INT_MIN - y)
and hope the optimizer turns it back into just checking the result. Or you use -fwrapv to concretize the ISO ambiguity and specify the natural two's complement semantics, checking overflow with the classic Hacker's Delight formula;
    ((x ^ s) & (y ^ s)) < 0

But the best way is to use the intrinsic __builtin_add_overflow or, depending on compiler support, its C23 standardization via <stdckdint.h> and ckd_add etc.

Well yeah that just means some aspects of the imaginary compiler were in some configurations approximated by some historical compiler versions and were in some cases rejected by the community (which cares about sane semantics even for behavior left undefined by ANSI/ISO) and in some cases left in as defaults but made trivially configurable for anyone who wants to define the undefined behavior.

Right, good example, and both GCC and Clang offer well understood parameters for deciding, per compilation unit, what behavior you want for signed overflow (-fwrapv, -fno-strict-overflow, etc), so in reality it's quite far from spooky arbitrary nasal demons.

Yet the standard does not tell you what the compilers do.

Linux works on a wide variety of platforms. It also relies on those platforms behaving predictably with respect to what the standard leaves undefined.

This description of ISO UB as a totally insane wonderland of random, malevolent semantics just doesn't describe reality.

This is a description of an imaginary compiler, evoked by the ANSI/ISO standards documents, which has never existed and will never exist. To understand what the program will do, you just have to understand the compiler behavior on your target platforms. A helpful intuition pump is: imagine the ANSI/ISO specifications simply do not exist; now what? Well, you just continue your engineering practice, the way you would for any of the myriad languages that never even had a post hoc standards document.

undefined behavior is the behavior of code patterns "for which this International Standard imposes no requirements" and the behavior is in fact almost always predictable and agreed upon by compiler vendors and the users of the language, which is why you are able to use programs that rely on undefined behavior probably every single second you are using the computer

edit: for example I'm typing this into Safari which means probably every key press and event is going through JSC JIT compiled functions—which have, structurally and necessarily and intentionally, COMPLETELY undefined behavior according to the spec—and yet it miraculously works, perfectly, because the spec doesn't really matter

If you stop trying to find something like truly ontologically novel about it, you might be able to understand what it actually is. Okay it's not impressive. It's not incredible. It's not groundbreaking new technology. It is what it is.

That kind of blanket demand doesn't persuade anyone and doesn't solve any problem.

Even if you get people to sit and press a button every time the agent wants to do anything, you're not getting the actual alertness and rigor that would prevent disasters. You're getting a bored, inattentive person who could be doing something more valuable than micromanaging Claude.

Managing capabilities for agents is an interesting problem. Working on that seems more fun and valuable than sitting around pressing "OK" whenever the clanker wants to take actions that are harmless in a vast majority of cases.

The solvents evaporate when the lacquer cures, right? A lacquered spatula or spoon could leach some plasticizers when heated up. But who on earth would go to the trouble of spray lacquering a spatula? It doesn't seem like a real concern. Wooden spoons from IKEA aren't gonna poison you!

Great! Feel free to ask questions or report problems on GitHub or the Fil-C Discord. If some package doesn't compile I can probably look into it!

FYI nginx and Apache and Postgres using shared memory across processes make them hard to use with Fil-C. Lighttpd works well though!

I've got a pure Go journald file writer that works to some extent—it doesn't split, compress, etc, but it produces journal files that journalctl/sdjournal can read, concurrently. Only stress tested by running a bunch of parallel integration tests, will most likely not maintain it seriously, total newbie garbage, etc, but may be of interest to someone. I haven't really seen any other working journald file writers.

https://github.com/lessrest/swash/tree/main/pkg/journalfile

I see what you mean, but I think it's a lot less pernicious than astrology. There are plausible mechanisms, it's at least possible to do benchmarking, and it's all plugged into relatively short feedback cycles of people trying to do their jobs and accomplish specific tasks. Mechanical interpretability stuff might help make the magic more transparent & observable, and—surveillance concerns notwithstanding—companies like Cursor (I assume also Google and the other major labs, modulo self-imposed restrictions on using inference data for training) are building up serious data sets that can pretty directly associate prompts with results. Not only that, I think LLMs in a broader sense are actually enormously helpful specifically for understanding existing code—when you don't just order them to implement features and fix bugs, but use their tireless abilities to consume and transform a corpus in a way that helps guide you to the important modules, explains conceptual schemes, analyzes diffs, etc. There's a lot of critical points to be made but we can't ignore the upsides.

I'd been imagining taking the Zig Language Server and adding some refactorings to it—it only had a bare minimum like Rename Symbol. It seemed like a huge project with so much context to get familiar with, so I put it off indefinitely. Then on a whim I decided to just ask GPT-5 (this was before Codex, even, I think?) to give it a go. Plopped it down in the repo and said, basically, implement "Extract Function". And it just kind of... did. The code wasn't beautiful, I could barely understand it, some of which must perhaps be blamed on the existing codebase not being exactly optimized for elegance, but it actually worked. On the first try! We continued to implement a few more refactorings. Eventually I realized the code we were churning out actually needs major revision and rewriting—but it took me from less than zero to "hey, this is actually provably possible and we have a working PoC" in, like, fifteen minutes. Which is pretty insanely valuable.

Interesting! I guess that's from your standard benchmark setup. Please note that Fil-C makes no secret of having a performance penalty. It's definitely a pre-1.0 toolchain and only recently starting to pick up some momentum. The author is eager to keep improving it, and seems to think that there's still plenty of low hanging and medium hanging fruit to pick.

It does (or did, at some point) pass the thorough SQLite test suite, so at least it's probably correct! The famous SQLite test coverage and general proven quality might make SQLite itself less interesting to harden, but in order to run less comprehensively verified software that links with SQLite, we have to build SQLite with Fil-C too.

If you missed it, djb himself posted this cute graph of "nearly 9000 microbenchmarks of Fil-C vs. clang on cryptographic software (each run pinned to 1 core on the same Zen 4)":

https://cr.yp.to/2025/20251028-filcc-vs-clang.html

I've heard Filip has some ideas about optimizing array performance to avoid capability checks on every access... doing that thread safely seems like an interesting challenge but I guess there are ways!

Yeah, but if you actually need to retain a live subgraph of the allocated heap, the arena can't help you. So you make an arena allocator that only frees its slab after moving out the reachable set to a new compacted arena. Congratulations, you've implemented a Cheney-style compacting GC!