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

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.

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.

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/

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.

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

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.

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!

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/

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.

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.

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.

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.

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

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.

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

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 as corresponding to classical states 0 and 1. If the qubit vector isn't in the 0 or 1 state, it's in some linear combination of them. This is called superposition. Since most people don't know what linear combination means, superposition is explained as "sort of both at the same time". Upon measurement the qubits are collapsed to 0 or 1 with some probability proportional to how close they are to the 0 and 1 states. The precise probabilities are given by something called the Born rule. I gave a longer talk aimed at computer scientists if you're interested beyond this explanation: https://youtu.be/F_Riqjdh2oM

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

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 than this: https://cdn.fosstodon.org/media_attachments/files/110/923/56...

Using a static site generator is surprisingly simple!

Undergraduate physics hasn't changed much in the past two years.

Using math to model a system instead of learning math qua math does wonders for ease of understanding. Derivates and integrals become easy if you're using them to model the relationship between position/velocity/acceleration. I don't think I really got linear algebra until using it to learn quantum computing.

(am also on the spectrum)

neuro-typicals mistake my intent and refuse to believe me

This is an idea I had to unlearn. We struggle as much understanding ourselves as understanding other people. When people react negatively to our behavior often times we immediately jump to extending unlimited benefit of the doubt to our own intentions. In reality, our perception of our own intentions are often post-hoc fabrications to preserve our self-image as a nice person. Letting go of this assumption was helpful to a better understanding of interpersonal interaction.

Time zones and shared language/culture disagree? Or if you think you can get a 90% margin on the competition with the same result, go start a company and see how that works out for you.

That's just... all of medical care. The procedures are almost all done by residents and, yes, med students under supervision of a full doctor. How do you think we get new doctors? Nobody wants to be the person who is used for teaching new doctors but that's how it is.

With each passing year my dread increases that this is all headed toward intensive solar radiation management schemes that will forever rob us of a beautiful blue sky. Anything to avoid real changes.

Incredible to post this in a year with record numbers of forest fires. When trees burn they release all their sequestered carbon. Climate change makes forest fires more common.

Regardless planting trees is still a good thing and I don't actually know of any liberals who are against it, very strange thing to believe of them.

These things are interlinked. Developing addiction or mental health issues makes you less able to keep an income. If housing is more expensive it's then that much easier to not be able to make rent. And if you're homeless then it's quite easy to develop drug addictions or mental health issues. Housing prices are a single dial that turns up the heat on the whole system.

Honestly we don't have to intellectualize this very much. A child can understand this. If housing is more expensive it will be harder for people to afford it! And people who can't afford housing become homeless!

The author cites the BNEF energy transition investment trends report a few times, and I encourage everybody to flip through it. It contains many interesting facts, and you certainly have to take an extremely skewed view to arrive at the same conclusions as the author: https://about.bnef.com/energy-transition-investment/

Notably, the banner fact that 2022 was the first year - ever - where global investment in renewables equalled investment in fossil fuels[1]. This was primarily championed by China, which produced one of the most astonishing graphs I've seen in recent times[2]. It entirely upended how I view leadership on this issue and what countries are taking it remotely seriously. Canada isn't even in the top 10!

Anyway, given that - again - this is the first time ever that investment in renewables has matched investment in fossil fuels, it is not surprising that fossil fuel usage has continued to grow.

[1] https://imgur.com/B2QBY6u

[2] https://imgur.com/OlMAKVd