Hacker News: ahelwer

New comment by ahelwer in "An ESPN producer who quit because of sports gambling"

ahelwer — Sat, 17 Oct 2026 23:18:11 +0000

I've stopped watching all sports because of this. You can't even talk about sports online now without some dull punter whining that their parlay didn't hit. It's nauseating. The gambling industry produces no value.

New comment by ahelwer in "Libreboot 26.10 "Ominous Olive" released with UEFI, Chromebook support"

ahelwer — Thu, 15 Oct 2026 22:43:28 +0000

Unfortunately it is. Thought the whole thing was a scam until six months ago. I think pretty highly of my development skills and have to be objective and admit I am outclassed in debugging and operational tasks now (and it isn't close). Writing non-script code isn't quite there yet (they are bad at abstraction) but I can't confidently predict how much longer that will be the case.

New comment by ahelwer in "OpenAI engineer arrested in bugging of executive conference room"

ahelwer — Tue, 13 Oct 2026 20:54:44 +0000

Interesting that they have a camera behind the TV, I suppose for this exact purpose.

New comment by ahelwer in "Terence Tao: Math 2.0 [pdf]"

ahelwer — Sun, 11 Oct 2026 20:46:31 +0000

I hope you are right but fear the reality might be more similar to Elysium, if not intentional depopulation. This is straying far into sci-fi but it might come down to whether AI escapes control of the ruling class and whether it is benevolent or not. The future looks like rule by those with money to fund the manufacture of robotic armies, if not.

New comment by ahelwer in "Terence Tao: Math 2.0 [pdf]"

ahelwer — Sun, 11 Oct 2026 17:03:44 +0000

There is a lot of that to be sure, but the bridge to a world where meals & health are not sustained through toil is completely missing. Hence the dark joking about escaping the permanent underclass. Nobody in any position of power is even hinting this is driving toward post-scarcity. It just looks like the same old vile maxim, all for ourselves, and nothing for other people.

New comment by ahelwer in "Former SR-71 engineer talks NASA's Blackbird revival program"

ahelwer — Mon, 05 Oct 2026 01:03:48 +0000

Unfortunately you might be out your good money, as the more plausible explanation is that current NASA administrator Jared Isaacman loves restoring & flying old airplanes (see https://en.wikipedia.org/wiki/Draken_International) and who wouldn't love restoring something as iconic as the SR-71?

New comment by ahelwer in "What's the future for pure math research in the age of AI?"

ahelwer — Sun, 04 Oct 2026 17:55:36 +0000

I like Wolfram and always enjoy reading his posts. An irreconcilable thing here is Wolfram clearly wants the Mathematica language to be central to the development of math as a field, but it's proprietary and so there is no guarantee it will survive the dissolution of the company if/when that happens. With Lean & others you can fairly safely assume that a particular version will be archived somewhere, and so a proof formalized for that version can be checked at any time. Not so with Mathematica. It's unfortunate, Mathematica is a cool language, but that's just the structure of incentives at this time. This is without getting into what a proof formalized in Mathematica would even mean, the relative maturity of the kernel and the possibility of there being multiple kernel implementations for cross-checking, and so on.

New comment by ahelwer in "What TLA+ can and can't check"

ahelwer — Thu, 01 Oct 2026 14:50:45 +0000

Many TLA+ users will tell you the greatest value of writing a spec was it forced them to think clearly about their system. However, thinking is very hard to sell, so we tend to center the razzle-dazzle about model-checking properties of your state space. Which is a great capability, don't get me wrong! Most non-trivial systems have a state space far larger than can be assessed for finding bugs via thinking.

New comment by ahelwer in "What TLA+ can and can't check"

ahelwer — Wed, 30 Sep 2026 21:25:19 +0000

It's a reasonable question. There are novel things I like about the syntax - like vertically-aligned conjunction & disjunction lists - but I don't really want to defend syntax that still uses all-caps KEYWORDS like it's the COBOL era and makes you use string values for enums. The underlying formalism is, however, amazing for thinking in, and it's used by P, Quint, and FizBee which all to varying degrees paint themselves as TLA+ successor languages.

I agree that spec/implementation conformance checking is also an issue. P has apparently had some success with PObserve for trace validation (checking whether the log of a running system is a valid execution of a P spec) but it is still not a well-known method with these tools in the same way that fuzzing or property-based testing have become. This requires some real product-level thinking to make usable and possibly full ownership of the system execution environment inside a VM or something like that.

New comment by ahelwer in "What TLA+ can and can't check"

ahelwer — Wed, 30 Sep 2026 19:57:46 +0000

You are quite close! That does indeed encode a limited form of reachability property - that P is reachable from at least one start state. As the article mentioned, these kinds of reachability properties are now actually available for TLC to check without having to jump through the hoop of negating it first.

A stronger type of reachability property is that a state is always reachable from every other state. This is useful in, for example, eventually-consistent systems where you want to know that your system always could converge to every replica having the same state, even though it never actually does converge unless all writes to the system stop. The article links to a post about how to specify & check those properties in TLA+ (it is possible!) but the way to do this is very much not ergonomic.

Editing to add "there exists a behavior where P is true" is probably meant to mean P is an arbitrary temporal formula. So you are correct that with the limited reachability property you identified, you can express the formula "there exists a behavior satisfying <>S". However, you cannot express anything other than simple formulas like that, not general temporal formulas.

New comment by ahelwer in "What TLA+ can and can't check"

ahelwer — Wed, 30 Sep 2026 18:45:19 +0000

This is true, and it falls into the "possible but not ergonomic" category for modeling systems like this in TLA+. Concurrent programs reading & writing to shared variables can be reordered at two levels: the compiler, and then the CPU. Specifying this in TLA+ is possible but difficult, and your conventional TLA+ specification will assume things happen in a linear order within each thread, and are interleaved arbitrarily between threads. In other words by default PlusCal works like there is both a barrier and memory fence between each action. Even with strong memory semantics like x86-TSO, specifying something like the action of the store buffer (where a core writes a value and can read the updated value but its write is not yet visible to other cores) requires actually writing your own tiny implementation of x86-TSO; there isn't one already defined as a library you can easily use.

I've been thinking lately about how to make this more ergonomic, as I've been getting into lock-free algorithms and would like to be able to specify them nicely in TLA+.

New comment by ahelwer in "1 in 8 cancer cases worldwide are caused by infections, study finds"

ahelwer — Tue, 29 Sep 2026 15:51:27 +0000

Unfortunately a lot of us will die in comparable ways if we are lucky enough to get that old. My grandmother was healthy & mentally with it until stroking out in her garden one day at the age of 90. That is the best any of us can hope for and the reality will almost certainly be far more painful and prolonged.

New comment by ahelwer in "The internet discovers TLA+. Now what?"

ahelwer — Sun, 27 Sep 2026 18:10:51 +0000

The last I learned of this was at the talk Temporal specification languages in industrial hardware verification by Simon Jantsch of Siemens at the ETAPS 2025 industry day track. Unfortunately I can't find the video posted anywhere, but predominantly the talk spoke of using proprietary symbolic model checkers for Linear Temporal Logic (LTL). It is reasonable to call TLA+ a successor to LTL, although LTL is definitely still used.

New comment by ahelwer in "The internet discovers TLA+. Now what?"

ahelwer — Sun, 27 Sep 2026 18:01:24 +0000

The state space you get when using real programming languages like Python is much, much larger than the one you get when abstracting your system design into TLA+. Thus when testing real systems you can only explore very small portions of the state space. This is a real thing people do, although it isn't yet widespread - the term to look for is deterministic simulation testing. Making a DST harness that can handle exploring an application state space without requiring large modification to the application itself is very challenging. Currently Antithesis are the only ones I know who have done it (disclaimer: no connection to this company, I just think they are very cool).

Can we have reachability properties in TLA⁺?

ahelwer — Sat, 26 Sep 2026 15:55:08 +0000

Article URL: https://ahelwer.ca/post/2026-09-26-reachability/

Comments URL: https://news.ycombinator.com/item?id=49857717

Points: 2

# Comments: 0

New comment by ahelwer in "Book review: Is parallel programming hard, and, if so, what can you do about it?"

ahelwer — Thu, 24 Sep 2026 19:58:49 +0000

That battle has unfortunately been lost and different sources give different definitions, often exactly swapped. This was discussed in one of the HN posts linked in the article: https://news.ycombinator.com/item?id=36318280

In the end I don't think it is too much of an issue. What confusion is really brought by conflating parallelism and concurrency? Sure, concurrent programs can be serialized onto a single core (that's how deterministic simulation testing implementations like Antithesis and record & replay implementations like Mozilla's rr operate). But there isn't some deep conceptual unlock you get by having a strict conceptual boundary between concurrency and parallelism.

Book review: Is parallel programming hard, and, if so, what can you do about it?

ahelwer — Mon, 21 Sep 2026 14:30:00 +0000

Article URL: https://ahelwer.ca/post/2026-09-21-concurrency-textbook/

Comments URL: https://news.ycombinator.com/item?id=49787759

Points: 149

# Comments: 66

New comment by ahelwer in "Omarchy: Any User Process Can Escalate to Root"

ahelwer — Sun, 30 Aug 2026 17:18:34 +0000

You need root in order to overwrite sudo in the first place I think, but yes password replay attacks are real. This is why I think it is a good idea to get a yubikey and use PAM to require a physical user presence check to acquire root privileges. You don't even need a password at that point. Unfortunately haven't figured out how to make this work over SSH.

The changing role of finite-state model checking

ahelwer — Mon, 24 Aug 2026 15:57:51 +0000

Article URL: https://ahelwer.ca/post/2026-08-24-finite-state-future/

Comments URL: https://news.ycombinator.com/item?id=49421639

Points: 4

# Comments: 0

New comment by ahelwer in "After two years of vibecoding, I'm back to writing by hand"

ahelwer — Mon, 26 Jan 2026 17:53:10 +0000

An alternative reading of these comments is "I went to the casino and had a great time! Don't understand how you could have lost money."