Viewing profile — ahelwer

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

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…

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 pred…

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…

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 l…

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, somethin…

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…

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 th…

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 li…

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 int…

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 …

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 compostin…

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

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 o…

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

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 t…

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 la…

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 in…

The shortest possible answer is that qubit states are modeled as two-dimensional vectors on the complex unit sphere. We arbitrarily designate two orthonormal vectors on this sphere…

You're talking about the difference between a scientist making like $50-150k/year salary and entities making millions or billions of dollars a year in profit. These are in no way c…

I hope this counts as productive feedback if the author of the blog is reading this - the post you put so much effort into writing truly deserves a better presentation experience t…