<rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Hacker News: reinitctxoffset</title><link>https://news.ycombinator.com/user?id=reinitctxoffset</link><description>Hacker News RSS</description><docs>https://hnrss.org/</docs><generator>hnrss v2.1.1</generator><lastBuildDate>Sun, 14 Jun 2026 21:58:31 +0000</lastBuildDate><atom:link href="https://hnrss.org/user?id=reinitctxoffset" rel="self" type="application/rss+xml"></atom:link><item><title><![CDATA[New comment by reinitctxoffset in "Formal methods and the future of programming"]]></title><description><![CDATA[
<p>No we're pre-alpha, I guess most people would call it stealth but it's more like, not quite done and we don't want to waste people's time because our entire thesis is around correct outcomes in AI systems at a level that permits their use in outcome-critical regimes (we sometimes call it "insurable" AI as a north star, would LLoyds of London or Swiss Re stand behind someone who was writing policies on this?).<p>Now a bunch of that is development tooling that copes with agent-scale software development, and a lot of that might become product surface, so we have a lot of usage denominated by like, bytes and agent hours and stuff because we build this stack in itself, but that's somewhat orthogonal to the north star vision.<p>We'll make sure to give the HN community the opportunity to see this stuff as early as anyone does if people find it interesting, most of the above will be open source fairly soon. Don't know if it'll make the front page, but the product will be called `ORBITAL`, so if you see that floating around that's us.<p>Appreciate the interest!</p>
]]></description><pubDate>Sun, 14 Jun 2026 20:28:15 +0000</pubDate><link>https://news.ycombinator.com/item?id=48532289</link><dc:creator>reinitctxoffset</dc:creator><comments>https://news.ycombinator.com/item?id=48532289</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=48532289</guid></item><item><title><![CDATA[New comment by reinitctxoffset in "Formal methods and the future of programming"]]></title><description><![CDATA[
<p>This is all pre-release but a few highlights:<p>- `continuity` is a `lean4` metaprogramming system that we use all kinds of ways but the real meat is it allows formal specification of codecs and state machines in ways that make security and performance properties proof amenable, the key trick here is to limit parser power to just what you need and no more. a very cool thing is that we can add targets to it, so when we do Zig for example, Zig will immediately get proven correct and frontier performance support for dozens of protocols that are not all mature right now.<p>- `libevring-cpp` (bound up into `libevring-hs` and `libevring-rs`) is a Trinity-inspired deterministic event replay system that replaces anything you would have done with `libuv` or whatever, and it's wired into `io_uring` (we're stuck with `kqueue` on darwin, eh). it interfaces with `continuity` machines and codecs (which are generated very carefully for the hardware they run on) and we have yet to find a way of measuring such programs where it doesn't resoundingly shatter the performance of any other asynchronous programming primitive in any language. i'm sure the community will prove us wrong when we release it, but it's real fast. and you get much stronger guarantees than in most such systems (Trinity derived, so if you can repro a bug, you can walk the event trace until it's sitting there in GDB and shit)<p>- `hyperconsole-cpp` (and `hyperconsole-hs` and `hyperconsole-rs`) is the TUI library idea taken to some deranged extreme on performance and supports everything in `notcurses`, it's pretty wild: <a href="https://youtu.be/YqgEtpJ8tGI" rel="nofollow">https://youtu.be/YqgEtpJ8tGI</a><p>- straylight-nix is a complete rewrite of nix that fixes thousands of bugs, hundreds of them security adjacent and dozens of them we only talk to vendors about. it's daemonless, dramatically faster, ground-up WASM-targeting compiler with a formal grammer, uses an extremely fast LSM-based store (it can read the legacy store but we don't write it) that fixes all the problems in floating CA, IFD is too cheap to care about, and recursive nix is no longer and issue (see daemonless). it supports tearing derivations into `REAPI` actions that you can feed to your friendly native NativeLink or whatever, which just goes through them like a woodchipper. KVM-based sandbox with snapshot and restore, really opens the world up on what your builders can be.<p>- `slide` is the reference implementation of a family of protocols called `SIGIL`: `SIGIL-LLM` is a binary encoding for LLM data that resets on ambiguity and drops the average bytes on the wire from e.g. OpenRouter to your harness from ~hundreds to ~1.5 per token, `SIGIL-API` is a bijection on OpenAPI 3.1.0 and AsyncAPI 3.0.0 that gives comparable improvements, and `SIGIL-SH` is such an encoding for a sensible subset of bash. this does about 1.5 billion tokens per second on a laptop and never emits partial frames, so you don't get speculative execution rollback problems in your harness that tilt agents off.<p>- `// WEAPON //` is an adversarial, vendor-skeptical, full-take surveilance agemt harness built on `hyperconsole-cpp` and `SIGIL` (so, you could absorb the entire token output of OpenRouter on one machine if you wanted at least on the wire and in the terminal, clearly the bottleneck rapidly becomes whatever the agents are calling, but it's `zmq4` transport underneath `SIGIL` so it's also trivial to full-take all of your data for fine tuning or whatever you want it for into e.g. `parquet` on R2. `// WEAPON //` does a bunch of stuff: the tool call surface is heavily optimized for AST-level edits that miss dramatically less, we intercept and manipulate shell commands (slice off the stupid `| tail -n5` that keeps the droid in a loop not seeing the error, pre-emptively ground using heuristics that have been tuned (defeats the search flinch), and always recovers from any stall, or nag box, or anything else that would serve as an unannounced rate limit, it's fine if vendors rate limit but they need to put it in their ToS. it has a bunch of other primitives, agents run in real KVM sandboxes and speculate out as wide as you want to pay the tokens for. we hyper-manage things like the cache breakpoint geometry of Anthropic so e.g. Opus rarely misses in cache and always hands off edits to specialized tool use models. it's pretty extreme the difference in outcomes relative to all this React jank.<p>- `s4` is a general-purpose compiler from most any pytorch 2.0 model to `myelin`-level performance on NVIDIA (we only support NVIDIA Blackwell at the moment, that might change) and it's never worse than `myelin` because if we don't out-tune it we invoke it, but we out tune it a lot because we've proven a lot of decideability theorems about tiling and scheduling on both 1CTA and 2CTA, so we can often arrive at a finite, enumerable set of schedule/tile choices. `myelin` mops up the random garbage around the big GEMMs just like in TRT-LLM.<p>- `sigil-trtllm` is inspired by TensorRT-LLM-Edge but designed from the ground up around Mellanox/ConnectX and in particular GPUDirect, so it can stream `SIGIL-LLM` tokens directly onto the wire whereas something like Dynamo is usually traversing both Python and NATS, which is super weird to us. this uses the `s4` compiler very heavily.<p>- `straylight-cas` is a geographically distributed content addressable store backed by any R2-compatible (so most any S3-compatible too) object store with multi-level LSM and extreme performance memtables, optimistic hinted handoff over `zmq4` to other geographies, and a really simple operational story, this is kind of the thing that powers the product surface.<p>... which is the thing i'm less ready to talk about because it's supposed to be a surprise.</p>
]]></description><pubDate>Sun, 14 Jun 2026 20:06:36 +0000</pubDate><link>https://news.ycombinator.com/item?id=48532055</link><dc:creator>reinitctxoffset</dc:creator><comments>https://news.ycombinator.com/item?id=48532055</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=48532055</guid></item><item><title><![CDATA[New comment by reinitctxoffset in "Formal methods and the future of programming"]]></title><description><![CDATA[
<p>I caught the religion on using types in conjunction with LLMs about eighteen months ago, but I only really got serious about `lean4` like six to eight months ago and now I wouldn't even consider using AI assist in software work with a `CIC` proof substrate that has practical C/C++ (and therefore, everything) FFI.<p>We've banned everything from JSON to Python, rewritten `nix` to have a compiler, and almost everything we write is not only property tested and multiply fuzzed to within an inch of it's life, but we have proofs in `lean4` that at a minimum drive property tests via `.olean` linkage, and when we have the bandwidth we prove exhaustiveness over the domain and property test that.<p>We skip the whole C++/Rust thing because all of the fast stuff is generated from `lean4` and so it doesn't really matter (C++ has advantages when bugs in it are actually bugs in `lean4` code, but you could go either way).<p>This is a big departure, and I certainly don't blame anyone who is skeptical: "ban JSON and Python wtf?!?!", but we've done millions of lines (checked) of this stuff and AI + formal systems is a dramatically bigger leap than no AI -> AI and Python. The latter in our experience is not monotone in progress, the former is almost always monotone in progress.<p>And you can do wild shit, this is a formal proof of the polyhedral tensor calculus that is modeled by things like ISL and CuTe, and using that we can get swizzling and tiling using `mdspan` in C++23 <i>on device</i> and prove it's right (up to some L'Hopital arugment about the coverage which this example doesn't demonstrate well: <a href="https://github.com/b7r6/mdspan-cute" rel="nofollow">https://github.com/b7r6/mdspan-cute</a><p>That in turn, well, it goes real fast. On the first try.<p><a href="https://straylight.software/assets/lambda-hierarchy.svg" rel="nofollow">https://straylight.software/assets/lambda-hierarchy.svg</a></p>
]]></description><pubDate>Sun, 14 Jun 2026 17:15:09 +0000</pubDate><link>https://news.ycombinator.com/item?id=48529831</link><dc:creator>reinitctxoffset</dc:creator><comments>https://news.ycombinator.com/item?id=48529831</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=48529831</guid></item><item><title><![CDATA[New comment by reinitctxoffset in "How to earn a billion dollars"]]></title><description><![CDATA[
<p>If you're not aware, in addition to being generally frowned upon on HN because it's zero-signal snark, the no doubt satisfying BU diss is also such a meme about socially awkward teenagers that it's a bit in a hit movie: <a href="https://www.youtube.com/watch?v=HtMmhcNKn0o" rel="nofollow">https://www.youtube.com/watch?v=HtMmhcNKn0o</a>.<p>At "Glad you agree" we've left plausible benefit of the doubt that you're arguing in good faith and so I'll bow out with one procedural grade discharge, which is that the LLM accusation is quite trivially prohibited in the stare decis of dang's rulings over the years, but still sometimes rallies downvotes, so my credentials as a human are that no LLM I'm aware of (and I work in AI) has  YouTube channels of code streams.<p>Chain of custody on that: <a href="https://news.ycombinator.com/item?id=48511333">https://news.ycombinator.com/item?id=48511333</a> -> <a href="https://www.youtube.com/@b7r6-c3t" rel="nofollow">https://www.youtube.com/@b7r6-c3t</a> so no, I'm not an LLM. I have Opus read my comments <i>after</i> I post them so I don't persist in trivial errors of reasoning, but I credit LLMs for their output just as I expect mine credited.</p>
]]></description><pubDate>Sun, 14 Jun 2026 16:12:06 +0000</pubDate><link>https://news.ycombinator.com/item?id=48528872</link><dc:creator>reinitctxoffset</dc:creator><comments>https://news.ycombinator.com/item?id=48528872</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=48528872</guid></item><item><title><![CDATA[New comment by reinitctxoffset in "How to Earn a Billion Dollars"]]></title><description><![CDATA[
<p>I wrote a 542 token rebuttal to his argument that you originally replied to, but to zoom in on that particular nub of a much more complicated picture:<p>No serious person acting in good faith disputes that new methods of wealth creation have started appearing at a dramatically higher rate in the last two or three hundred years than any precedent before that. Everyone, including AOC (who I agree with in this instance but am not in general a huge fan of, just to be clear, I can respect a person's credentials without blindly endorsing them), would concede that point cleanly unless they were trolling.<p>The second point is so ill-formed as to verge on oxymoronic when examined against either of mechanism on the ground or Bayesian prior of history. New methods of wealth creation have triggered market failures admitting new methods of <i>wealth centralization</i> a number of times in recent history, the Gilded Age being perhaps the poster child for this failure mode, and the Great Depression being perhaps the poster child of the magnitude of that failure mode.<p>The sleight of hand here is recursive, the two points are one that is trivially true followed by the shellcode that looks like a test fixture, and the shellcode is a subtle rename, `s/time bash -c 'my-command'/sudo bash -c 'my-commmand/`. It's almost reasonable, except that it grants arbitrary privileges to something that definitely shouldn't have arbitrary privileges.<p>In both instances, pg is smart enough to know he's arguing in bad faith.</p>
]]></description><pubDate>Sun, 14 Jun 2026 15:37:59 +0000</pubDate><link>https://news.ycombinator.com/item?id=48528380</link><dc:creator>reinitctxoffset</dc:creator><comments>https://news.ycombinator.com/item?id=48528380</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=48528380</guid></item><item><title><![CDATA[New comment by reinitctxoffset in "How to earn a billion dollars"]]></title><description><![CDATA[
<p>My copy of Hackers and Painters is the first printing, I'm extremely versed in the last twenty years of pg's writing and public speech, <i>and the glowing arc of that thought over that time</i>.<p>Early pg wrote about Lisp and engineers should do their own testing and commodity FreeBSD on commodity Intel was better than Oracle on Sun for starting a company.<p>He wrote that makers and managers needed different schedules. He wrote that math has asymmetrical upsides. He wrote that you do things that don't scale while you're in the garage.<p>In his wheelhouse he was best in the genre, maybe not the Balzac he fancies himself as an essayist or the painter he fancies himself at all, but the best guy to listen to if you were doing a garage band startup that involved the Internet. He was surrounded by legitimate legends like Robert Tappan Morris and Trevor Blackwell, and he wrote about things he understood.<p>Late Soviet Paul Graham exists as the lobbyist for Garry Tan Y-Combinator, which isn't even really prestigious anymore. As far as the signalling value goes? I'd rather have a strategic from NVIDIA before YC. I would think about YC's money if literally no one else was interested. This is "ChatGPT Tha License Dawg", "die motherfuckers die motherfuckers die" tweets tagging elected officials Y-Combinator he's defending, and the vampire companies he cites as his clean wins are suitable filleted in the rest of the thread that mine would be redundant.<p>And the real mile marker of a guy whose audience has exceeded his depth is that he's lecturing a room full of people about how a single operation on the iPhone calculator app can teach you more about government and economics than is apparently understood by someone who has survived eight years in Congress designed to destroy people like her, who has an Economics degree cum laude from Boston University that she got while working as a bartender to support herself and her family after her father died, a situation with no parallel in pg's life or that of anyone adjacent to him in either it's highs or lows.<p>I got into this business substantially because pg's writing was so motivating to twenty year old me, and for that I'm still grateful. And just like I hope Kanye gets back on his Lexipro and starts making great music again, I hope that pg goes back to his roots and starts printing great technical and startup essays again instead of spewing solid waste.<p>But just like I can't follow Kanye down the "death con three to the jews in hollywood" road, I can't follow pg down the "think about the billionaires and don't listen to the honors economist multiple-term congresswoman" road.<p>One is dramatically more offensive in it's form, one is dramatically more toxic in it's substance, because there are people who take it seriously.</p>
]]></description><pubDate>Sun, 14 Jun 2026 15:09:57 +0000</pubDate><link>https://news.ycombinator.com/item?id=48527969</link><dc:creator>reinitctxoffset</dc:creator><comments>https://news.ycombinator.com/item?id=48527969</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=48527969</guid></item><item><title><![CDATA[New comment by reinitctxoffset in "How to earn a billion dollars"]]></title><description><![CDATA[
<p>There's an older tradition of thought on the matter with better intellectual pedigree and epistemological hygiene: "Behind every great fortune lies a great crime."<p>The easiest way to earn a million dollars is to start a business that makes sense and work your ass off running it well. Maybe that's even the easiest way to reliably earn ten million dollars, a million isn't what it used to be.<p>But at some scale that's far short of a billion the game becomes about  <i>asymmetry</i>.<p>This asymmetry takes many forms. For Steve Cohen it was trading on inside information, for Jim Simons it was (as far as anyone can tell) novel mathematics.<p>For most of the technology companies in the 21st century it was about privatizing the commons and/or externalizing costs that a well-refereed market would place on your company.<p>The United States used robust public/private partnerships and a vibrant, thriving university system to build the greatest pile of latent wealth in the sum history of humanity during the 20th century. Everything from the transistor to the integrated circuit to the laser to Velcro to tang to the internet to the web was a product of this holy Trinity of innovation: defense and related public money, well-refereed private companies (even a notable natural monopoly or two under muscular regulation), and a paved path between the Academy and the other two. The gains accrued enough to individuals to keep everyone motivated but largely in the form of <i>status</i>, which confers a desirable station in life but does not compound directly into political power. Feynman and von Neumann and Einstein all seem to have led very enviable lives and are easily as smart and accomplished as anyone in the front row at the last Inauguration (and if we're honest, a lot more), but none of them had a billion dollars or untoward access to the levers of government. All of them paid far more <i>into</i> the ocean of latent wealth deeded to the body politic than they took <i>out</i> of it.<p>And at some point (my money is on the kneecapping of Brooksley Born, whose architect is now resigning in disgrace from everything for Epstein affiliation and whose most recent post was on the board of pg's protege) the flow reversed. The access caste started to be d away from the competence caste and the singular fortune deeded to the public started to accumulate as a dozen private fortunes <i>that were substantially just the 20th century stuff with a named owner</i>.<p>You get a billion dollars by stealing it, this is qualitatively different, a distinction of kind not of degree, from how you get a million or even a few tens of millions.<p>To get a trillion dollars as we have now seen, well first you steal a billion.</p>
]]></description><pubDate>Sun, 14 Jun 2026 12:47:49 +0000</pubDate><link>https://news.ycombinator.com/item?id=48526730</link><dc:creator>reinitctxoffset</dc:creator><comments>https://news.ycombinator.com/item?id=48526730</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=48526730</guid></item><item><title><![CDATA[New comment by reinitctxoffset in "Making Claude a Chemist"]]></title><description><![CDATA[
<p>Organic chemistry seems like a discipline better done by chemists than forward deployed staff with their payoff function sharply truncated at an IPO which at this point may or may not happen on schedule.</p>
]]></description><pubDate>Sun, 14 Jun 2026 06:48:31 +0000</pubDate><link>https://news.ycombinator.com/item?id=48524797</link><dc:creator>reinitctxoffset</dc:creator><comments>https://news.ycombinator.com/item?id=48524797</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=48524797</guid></item><item><title><![CDATA[New comment by reinitctxoffset in "The computer science degree isn’t dead"]]></title><description><![CDATA[
<p>The sibling commenters are correct but I will add with the benefit of being an old guy that this ebbs and flows. GP said "I have never seen tech be less about engineering", and I agree.<p>But it can't get much <i>less</i> about engineering before rich people become poor in large numbers, and that will start the pendulum back the other way.<p>Rich people losing money that matters in large numbers is like a soft civil war, everything changes.</p>
]]></description><pubDate>Sat, 13 Jun 2026 22:26:07 +0000</pubDate><link>https://news.ycombinator.com/item?id=48522118</link><dc:creator>reinitctxoffset</dc:creator><comments>https://news.ycombinator.com/item?id=48522118</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=48522118</guid></item><item><title><![CDATA[New comment by reinitctxoffset in "I think they are lying to you [video]"]]></title><description><![CDATA[
<p>I read this a lot and it is just very foreign to me. I use AI systems in software work all day seven days a week and my job has become simultaneously more interesting and more difficult because I scale the ambition up until it's hard again.<p>Isn't anything else a surrender to irrelevance? I agree that many coding tasks that were previously effort intensive are now not effort intensive, but there's no ceiling I'm aware of on how correct and performant and economical and capable software can be short of saturating the hardware.<p>And the emergence of agentic intelligence at scale demands new regimes of performance and correctness and economy like maybe nothing else ever has.<p>I have an anecdote related to TUI flickering in that my TUI library had a flickering problem because it was doing more than 10k FPS, and so I had to lock the buffer swap to the vsync to stop it tearing.<p>AI coding didn't make more React too cheap to meter, it made notcurses bound into Trinity-inspired deterministic replay event substrate over io_uring <i>possible</i>.<p><a href="https://youtu.be/YqgEtpJ8tGI?feature=shared" rel="nofollow">https://youtu.be/YqgEtpJ8tGI?feature=shared</a></p>
]]></description><pubDate>Sat, 13 Jun 2026 01:18:34 +0000</pubDate><link>https://news.ycombinator.com/item?id=48511333</link><dc:creator>reinitctxoffset</dc:creator><comments>https://news.ycombinator.com/item?id=48511333</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=48511333</guid></item><item><title><![CDATA[New comment by reinitctxoffset in "Why AI hasn't replaced software engineers, and won't"]]></title><description><![CDATA[
<p>In every regime where we have meaningful longitudinal data about the long run outcomes of introducing technology that is superhuman at some or all of a human's job, the combination of the machine and an expert human outperforms either alone, with probably the clearest parallel structurally being chess, though this is true of all of the hard sciences and all of frontier engineering (semiconductor design).<p>There will never be a human who can beat Stockfish ever again, digital intelligence has simply accelerated  away from human intelligence in that regime.<p>There is no other human alive who can beat Magnus Carlsen. Stockfish crushes Magnus.<p>But Magnus and Stockfish playing together crush any conceivable combination of just human or just computer. And no serious chess player would train without a computer or decline the assist if the contest mattered.<p>And this is in a regime where the dominance of the machine is total, structural, and permanent, far more so than any existing AI's impact on the outcome distribution of any recent development on any white-collar knowledge work include even the most sophisticated software engineering done anywhere. The demonstrated as opposed to <i>completely conjectural</i> lift on SWE outcomes with Claude Code (and even that's controversial, let's take the high end of the claims) is real and changes the geometry of the situation not at all.<p>Nor is there any apparent limit on how much arbitrarily sophisticated software the world has an appetite for, you could take someone at the absolute top of the field (I'm a big Carmack fan let's go with Carmack), and give him cutting edge AI assist, and the best program a person can write just got better. Sweet!<p>And this applies anywhere from junior to Carmack: however good they were, they're better now. We can build harder things. We can have extreme quality software where previously we were stuck with some Electron jank, across the board. Does anyone think Slack would lose market share if it went back to its gaming roots and was gorgeously 3D accelerated on every surface against a backend that could instant and perfectly synchronize an arbitrary workspace on a flakey cell connection and never have an outage or data loss? Or would they rapidly shred the remaining competition and become the favored tool of everyone?<p>In adversarial regimes like trading or drone warfare, you better believe the best hackers have arbitrary assist if you're going to play against them.<p>I think the thing to be hand-wringing about isn't AI, it's that capitalism no longer seems to be an adversarial regime. The worst software rivalries in the industry look more like a pillow fight than a battle of will.<p>And if there is any lasting reduction in headcount, it's leaders lacking ambition agreeing tacitly to not play very hard, not AI, that is to blame for that. None of the HFT shops nor amusingly the frontier labs have reduced their hiring or compensation at all. If anything, it's going up!</p>
]]></description><pubDate>Thu, 11 Jun 2026 14:26:57 +0000</pubDate><link>https://news.ycombinator.com/item?id=48490823</link><dc:creator>reinitctxoffset</dc:creator><comments>https://news.ycombinator.com/item?id=48490823</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=48490823</guid></item></channel></rss>