polyglotfacto
Joined 6 years ago
Karma
201
Submissions
72
Member since
Apr 11
Recent submissions
Comment · 2 months ago
Comment · 7 months ago
I implemented MessagePort in Servo back in 2019 — it was the hardest concurrency problem I'd encountered, because ports can be transferred between event loops while messages are still in flight. This weekend I finally got around to formalizing it in TLA+, with Claude helping with the typing.
The interesting outcome: the abstract spec (following the HTML standard) is so simple that the refinement proof itself serves as the inductive invariant. No additional invariants needed. TLC found no bugs in the Servo implementation, though it did help me make explicit a sequencing assumption that was implicit in the code.
Happy to answer questions about the TLA+ approach or the Servo implementation.
Comment · 8 months ago
I've been implementing the WebNN Web Standard on a personal Servo branch with AI coding assistance (main bans AI), and switched to GPT 5.4 this week. It introduced a race condition that compiled cleanly, passed tests, and would have been hard to catch if calling patterns had ever changed — and separately produced over-engineered architecture that took several iterations to unwind. Both episodes say something interesting about where agentic coding actually breaks down. Article includes the conversation transcripts.
Comment · 8 months ago
I am in the third week of my experiment with AI-assisted coding on a personal branch of Servo (which still bans all AI contributions).
First, the least relevant metric: LOC. Almost doubled from 7k to 12k in a week.
Current WPT pass rate, compared to the default integration of rustnn (pywebnn) is at: https://gist.github.com/gterzian/95371d56468390177982c068480...
This week was the grunt work: grinding through the long list of missing operations, with almost all now implemented.
Also switched to a more expensive coding model (GPT 5.3 Codex), which was an improvement, but there were still a few clear fails—specifically around the model taking "shortcuts" with spec logic.
Comment · 8 months ago
I’ve used TLA+ for six years to "debug my thinking," but I always treated the jump from spec to implementation as a leap of faith.
What surprised me in this experiment with Lean was that the AI-assisted formalization actually caught an error in my "vetted" TLA+ spec that had been sitting there for two years. It turns out my inductive invariant wasn't strong enough—something the TLA+ model checker didn't slap me for, but Lean’s kernel refused to ignore.
This was also a way to bridge a higher-level spec, written in Lean in a kind of TLA-like flavor, and the lower level implementation, also written in Lean but with a code-like flavor, and then proven that the implementation refines the spec.
Using Lean to bridge the gap between high-level temporal logic and low-level IO implementation, all written by AI but driven by human intent, feels like the first time the "coding singularity" might actually lead to better software rather than just more software
Comment · 8 months ago
I am a maintainer of the Servo web engine. Two years ago, our project banned AI-generated contributions. I was a dissenting voice on that policy, and have continued to experiment with AI on side-projects. This is perhaps the most ambitious side-project so far: implementing the WebNN (Neural Network) API.
Given the policy in place, I'm doing this on a personal branch of Servo. I’m using it as a sandbox to test a specific thesis: AI is not an architect; it is a "fluid syntax engine."
This is also my response to the "autonomous slop" seen in projects like fastrender that claim to build complex software with AI but produce what I call "fine-looking nonsense" (see https://news.ycombinator.com/item?id=46624541#46709191). I wanted to see if a human architect could use an AI agent to handle the syntax and boilerplate of a Web Standard while the human retains total control over the conceptual structure.
Progress & Tech Stack:
The scope: I am using `rustnn`, and this project can be seen as doing for the Web what `pywebnn` does for Python.
The model: I am intentionally using a "cheap" LLM: Raptor mini.
The scale: I’m 7k LOC into the implementation. It currently passes a subset of WPT (Web Platform Tests) conformance tests for a specific operator (and its dependencies): add. Such a conformance test requires implementing the full graph compilation and dispatch workflow. Code is at https://github.com/gterzian/servo/compare/master...gterzian:servo:webnn
The backend: The work involves integrating the `rustnn` library into Servo’s runtime, with compute currently happening only via CoreML (macOS only).
You can read the full breakdown of the first week and a half (contains links to code and various illustrative commits) in the link for this post.
And the backstory on why I'm doing this is at: https://medium.com/@polyglot_factotum/the-slop-diaries-imple...
I’d be happy to hear from others on how they balance the "syntax speed" of AI with the "architectural integrity" required for long-term projects.
Comment · 8 months ago
Within the Federal Reserve System, we have also been exploring the use of AI in our own operations and have established an AI program and governance framework for the use of AI technologies. One internal application of GenAI that shows considerable promise is technology modernization. Within clear guardrails, we are using GenAI tools to translate legacy code, generate unit tests, and accelerate cloud migration. So far, the result of this usage is faster delivery, improved quality, and an enhanced developer experience. In one recent project updating hundreds of databases, AI tools helped cut the time to complete this type of work by 50 percent, detected and resolved 30 percent more issues during testing compared to previous migrations, and enhanced team focus on higher-value coding work. My sense is that these are the kinds of uses and the scale of success that many businesses are experiencing.
I'm using headless Pi with my own UI and sandbox client, https://github.com/gterzian/uni03C0, as well as a bunch of Pi extensions for things like accessing Web standards and browser use via CDP for testing.
Switching to 4.1 today...
Edit: it seems they pushed the date at which they route the Pro calls to new Flash, so today I ended up paying regular Pro rates thinking I was using the new Flash; an example of how their offering is not quite as predictable as I would like it to be (the other is cache performance being unpredictable).