Hacker News: ahelwer

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."

New comment by ahelwer in "The current state of TLA⁺ development"

ahelwer — Fri, 16 May 2025 21:24:32 +0000

There is a strong Jevons Paradox effect at play here though, people generally have a set amount of wall-clock time (1 minute, 10 minutes, etc.) they budget to check their model and then find the largest model that fits within that wall-clock time. So really this just increases the size of the state space people will explore, which might be the difference between checking, say, 3 vs. 5 nodes in a distributed system.

New comment by ahelwer in "The current state of TLA⁺ development"

ahelwer — Fri, 16 May 2025 02:31:34 +0000

That's very neat! I will look at Truffle. The TLA+ interpreter is definitely "weird" in that it does this double duty of both evaluating a predicate while also using that same predicate to extract hints about possible next states. I wonder how well this highly unusual side-effectful pattern can be captured in Truffle.

Edit: okay the more I look into GraalVM the more impressed I am. I will have to sit down and really go through their docs. Oracle was actually cooking here.

New comment by ahelwer in "The current state of TLA⁺ development"

ahelwer — Fri, 16 May 2025 00:55:28 +0000

Hillel Wayne wrote https://learntla.com/ which is quite good! Leslie Lamport also has a webpage of other possible learning resources, including a video course he put together where he wears many strange hats: https://lamport.azurewebsites.net/tla/learning.html

Personally I learned by reading the first few chapters of Specifying Systems.

New comment by ahelwer in "The current state of TLA⁺ development"

ahelwer — Fri, 16 May 2025 00:36:14 +0000

There are some proposals floating around to evolve PlusCal. Probably the most prominent is Distributed PlusCal[0]. There's a programming language lab at UBC which is also doing a lot of experimentation with transpiling PlusCal to Golang[1]. They presented a paper at the latest community event.

The PlusCal-to-TLA+ transpiler is considered part of the core TLA+ tools and will definitely keep being maintained.

[0] https://conf.tlapl.us/2020/03-Heba_AlKayed-An_Extension_of_P...

[1] https://distcompiler.github.io/

New comment by ahelwer in "The current state of TLA⁺ development"

ahelwer — Fri, 16 May 2025 00:33:20 +0000

There has definitely been a focus on improving developer onboarding in the past few years! If someone's PR is rejected now that can be considered a failure of the process, something to be fixed. I think when TLA+ was mostly a product of MSR this sort of thing could kind of fly (still unfortunate) but now that we're out in the wild with a foundation it's really a survival thing to not bounce willing contributors.

New comment by ahelwer in "The current state of TLA⁺ development"

ahelwer — Thu, 15 May 2025 20:43:30 +0000

Hillel Wayne wrote a post[0] about this issue recently, but on a practical level I think I want to address it by writing a "how-to" on trace validation & model-based testing. There are a lot of projects out there that have tried this, where you either get your formal model to generate events that push your system around the state space or you collect traces from your system and validate that they're a correct behavior of your specification. Unfortunately, there isn't a good guide out there on how to do this; everybody kind of rolls their own, presents the conference talk, rinse repeat.

But yeah, that's basically the answer to the conformance problem for these sort of lightweight formal methods. Trace validation or model-based testing.

[0] https://buttondown.com/hillelwayne/archive/requirements-chan...)

New comment by ahelwer in "The Stallman Report"

ahelwer — Mon, 14 Oct 2024 15:13:19 +0000

I think it is good that people put in a lot of effort to collect this in one place. The report opens with a very strong perspective:

>The case against Stallman is clear, and yet the free software community has failed to act, in particular at the level of institutions and leadership but also in the form of grassroots support for Stallman. Many defenses of Stallman rely on a comfortable ignorance: ignorance of the scope and depth of Stallman’s political campaign against women and victims of sexual violence, or a comfortable belief that Stallman ceased his problematic behavior following his 2021 re-instatement in the Free Software Foundation. Some believe that Stallman’s speech has not caused material harm, or that his fringe views are not taken seriously; we provide evidence to dismiss all of these arguments in this report.

One thing I have consistently encountered when discussing contentious topics with people is that intentional ignorance is a tactic. One cannot be held responsible for acting one way or another on an issue if they do not know anything about it. Women I know in industry report this as by far the most common reaction of male coworkers to one of their colleagues facing allegations of sexual harassment. They don't know anything about it, it seems complicated, they haven't followed it closely, they don't want to get involved, etc. It is very frustrating and I am glad the report has identified this phenomenon and is pointing out this has been going on for long enough that it cannot be reasonably deployed by anybody.

New comment by ahelwer in "The Little Typer (2018)"

ahelwer — Sat, 28 Sep 2024 19:33:58 +0000

This series of books has always been aimed at people who want to implement the underlying systems. If you’re more interested in the application side of dependent types you might like the book Functional Programming in Lean by the same author, which is freely available online!

New comment by ahelwer in "The Little Typer (2018)"

ahelwer — Sat, 28 Sep 2024 16:18:57 +0000

I worked through this a few years ago and it is wonderful, but I found chapter 9 on the replace function totally impenetrable, so I wrote a blog post in the same dialogue style intended as a gentler prelude to it. A few people have emailed me saying they found it and it helped them. https://ahelwer.ca/post/2022-10-13-little-typer-ch9/

TLA⁺ is more than a DSL for breadth-first search

ahelwer — Wed, 18 Sep 2024 16:57:45 +0000

Article URL: https://ahelwer.ca/post/2024-09-18-tla-bfs-dsl/

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

Points: 9

# Comments: 2

TLA⁺ Unicode support: Learning to work with others in open source

ahelwer — Tue, 28 May 2024 17:01:22 +0000

Article URL: https://ahelwer.ca/post/2024-05-28-tla-unicode/

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

Points: 3

# Comments: 0

New comment by ahelwer in "'Meditations' by Marcus Aurelius – Stoicism in Modern Language [video]"

ahelwer — Fri, 12 Jan 2024 17:51:55 +0000

Good way to describe it. I tend to see it occur on lists alongside The Art of War and The Prince, which have this weird reputation as titanic, dense tomes read by Serious Men but in reality are more like pamphlets that you can go through in about half an hour. The first time I saw a copy of The Art of War in person I actually laughed out loud.

New comment by ahelwer in "The University of California has all but dropped carbon offsets"

ahelwer — Thu, 30 Nov 2023 16:25:10 +0000

This is a great passage but in a society taking climate change seriously carbon farming will unironically become a thing. Planting certain crops or using certain forms of composting to sequester as much carbon as possible on large areas of land that are not used to produce food or other cash crops.

New comment by ahelwer in "The University of California has all but dropped carbon offsets"

ahelwer — Thu, 30 Nov 2023 16:15:32 +0000

All modeling suggests that applying both of these tools together (incentives & disincentives) is multiplicatively more effective than applying either on its own. Taxing emissions means those emissions still happened.

New comment by ahelwer in "The University of California has all but dropped carbon offsets"

ahelwer — Thu, 30 Nov 2023 15:57:41 +0000

Go ahead and buy the land & oil rights to a large oil reservoir if you want to cash in on this hypothetical program.

Paying off the oil companies in this way means the end of the oil companies. They get a one-time cash infusion but that's it, no recurring revenue. Then no more oil companies to lobby against climate change. It's the only non-revolutionary route left, probably. Oil companies aren't just going to stop pumping oil and stop throwing the government around.

New comment by ahelwer in "The University of California has all but dropped carbon offsets"

ahelwer — Thu, 30 Nov 2023 15:55:08 +0000

It's an actual published paper you can read, not something KSR made up.

New comment by ahelwer in "The University of California has all but dropped carbon offsets"

ahelwer — Thu, 30 Nov 2023 15:33:56 +0000

If you're still committed to technocratic market-driven solutions to climate change there's the interesting idea of Carbon Quantitative Easing, essentially directly paying people to not emit carbon (read: pay oil companies to not pump out the oil they're going to pump out) or to sequester carbon with various methods. It's thought of as a carrot along with the stick of carbon taxes adding a cost to emissions.

First learned about this in the excellent sci-fi novel The Ministry for the Future.

https://en.wikipedia.org/wiki/Carbon_quantitative_easing

New comment by ahelwer in "Wrangling Monotonic Systems in TLA+"

ahelwer — Thu, 02 Nov 2023 13:06:33 +0000

It is be interesting to think of how a checker would work that detects monotonicity & deploys this theorem to check liveness properties. Maybe I'm just describing the TLA+ proof language! Also something to bring up at the next monthly TLA+ meeting.

New comment by ahelwer in "Wrangling Monotonic Systems in TLA+"

ahelwer — Wed, 01 Nov 2023 23:03:35 +0000

That's an interesting idea about a built-in ordered opaque value type. You should bring it up at the next monthly TLA+ foundation community call on November 14th![0] It would be interesting to hear peoples' feedback on it.

[0] Details hidden in the google calendar link on this thread in the mailing list: https://groups.google.com/g/tlaplus/c/CpAEnrf-DHQ/m/YrORpIfS...