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.
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/
This is great for me for a completely auxiliary reason, which is that I wanted to know whether this was just gonna be a book about programming Fibonacci numbers into types or some ish... and in some ways it's kinda worse, at chapter 9 you are still proving that different takes on x→x+1 are the same. (But using rewrite rules seems kinda interesting in the abstract I guess.)
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!
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.
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.
I read up until about this point in the book, but frankly I stopped because I lost confidence that KSR had any idea what he was talking about when it came to central banks, and more broadly finance in general.
Maybe someone here can help me understand, what exactly is the point of "carbon quantitative easing" over a straightforward carbon exchange? Maybe the government buying and selling carbon allowances (out of thin air) on the exchange makes this "quantitative easing", but I would avoid implying it's monetary policy when it seems like it's clearly fiscal policy.
Even more confusing to me was how KSR's "carbon coin" plays into all this. It seems like dollars would work fine. Euros if you want. Introducing some new world currency just seems like it's throwing a huge wrench into an already controversial issue.
I think market-driven solutions to climate change are an exciting possibility, but I just didn't understand what he was going for here.
I'm aware it's a "real" paper. I did try reading it, but I stopped since it didn't seem to answer any of my questions. I'm not an academic, and certainly not an academic in the field of economics or monetary policy, so maybe I'm just too stupid to understand it.
That said, I think my question is pretty basic and easy to anticipate, so I was disappointed I couldn't find it addressed in (relatively) simple terms.
As far as it being a "published" paper, my recollection is that it looked like the paper was self-published. I could be wrong about the self-publishing thing, but as far as I'm aware it's not published by any kind of reputable academic journal.
That’s never sat right with me. I don’t pump any oil out the ground personally now, but I’m thinking about starting. What area of the country would be best for me to decide to not pump oil and cash in on this program? Should I not pump oil from both Alaska and the Gulf, in order to diversify my non-operations? Or maybe start smaller and just not pump in the Gulf to get started, and only later expand to also not pumping in Alaska?
It seems far better to pay carbon dividends to people (only humans, not fictional people) and then charge for carbon emissions (not the extraction of fossil fuels; you’re welcome to pull it out and put it in a tank paying only the emissions of your extraction equipment, but when someone buys it to consume, they pay the carbon cost.)
Tweak the dividends and carbon costs as needed to achieve the balance of policy goals.
His specialty was alfalfa, and he made a good thing out of not growing any. The government paid him well for every bushel of alfalfa he did not grow. The more alfalfa he did not grow, the more money the government gave him, and he spent every penny he didn't earn on new land to increase the amount of alfalfa he did not produce. Major Major's father worked without rest at not growing alfalfa. On long winter evenings he remained indoors and did not mend harness, and he sprang out of bed at the crack of noon every day just to make certain that the chores would not be done. He invested in land wisely and soon was not growing more alfalfa than any other man in the county. Neighbours sought him out for advice on all subjects, for he had made much money and was therefore wise. “As ye sow, so shall ye reap,” he counselled one and all, and everyone said “Amen.”
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.
Well, presumably you'd only get paid to not-drill if you otherwise had the drilling rights? So if you bought the rights to extract from an oil field in Alaska or the Gulf, you could get paid not to use them. That seems reasonably coherent to me, although maybe I'm missing something big.
That said, I think I also prefer the idea of achieving these goals by tweaking the price of carbon. But again, maybe I'm missing something.
I read an article that suggested the government buy oil companies in order to manage their decline. Obviously nationalizing an industry is a huge deal and a pretty drastic step, but the argument seemed reasonable and if more lightheaded attempts to solve the climate crisis continue to fail I don't think that should be off the table.
> Well, presumably you'd only get paid to not-drill if you otherwise had the drilling rights? So if you bought the rights to extract from an oil field in Alaska or the Gulf, you could get paid not to use them.
At least in the U.S., extraction operations are usually organized as LLPs--more specifically MLPs, where partnership stakes are publicly traded. This means anybody can easily acquire drilling or extraction rights with a simple online transaction, just like they can with corporate stock.[1] Whatever flaws a pay-to-abstain system has will be exploited at least as fast as any other easily exploited financial incentive scheme.
Even excluding publicly traded MLPs, the market for buying + selling partnership interests in drilling operations is remarkably liquid, at least in the U.S. and especially for long-established fields such as in Texas or California, which are perhaps the operations that could most easily exploit a pay-to-abstain incentive scheme by, e.g., overestimating their reserves. (New fields would be even easier to overestimate, but that could in large part be addressed by avoiding the scheme entirely and simply preventing extraction ahead time--e.g. by stopping the sale of Federal mineral rights, or using environmental laws to prohibit extraction, which is more easily done before an extraction operation is established.)
[1] The reason for this is various tax incentives which make direct ownership stakes and their passthrough income and deductions the most profitable investment structure. But the Schedule Ks are really annoying when doing your taxes. AFAIU an MLP is similar to an REIT (Real Estate Investment Trust), the purpose of which is also to provide an easily traded investment providing passthrough income and deductions. REITs have become notorious for effectively accelerating the exploitation of flawed real state regulations, policies, and taxation. They're not per se bad, but more efficient financial markets cuts many ways.
This plus many people own mineral rights that are impractical or likely non-economical to exercise if you have to actually do the work to get the resource out of the ground. If you take that obligation to zero, many more properties' mineral rights are valuable (which goes to the exploitable financial incentive scheme point you made).
I own the mineral rights to a plot that also has a house on it. It would suck for the house usage to drill for oil on that land and there might not be economically viable oil underneath (you only ever know statistically/via modeling until you drill)...
I'm sure there would be challenges. In a lot of ways, they seem like the same challenges that have always faced OPEC.
It does seem like a scenario where you don't really want the efficiencies markets discover, which is why I mentioned the nationalization option. Not to suggest that option should be taken casually, or wouldn't come with its own set of challenges.
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.
You think that bribing oil companies to not extract oil temporarily is a more effective financial lever than taxing emissions on an on-going (and escalating, if policy goals require that) basis? That seems as if we’d be prioritizing the needs of the oil companies and shareholders over those of the actual humans on the planet.
I think the arguments for leaving oil in the ground have more to do with path dependence than prioritizing the needs of oil company shareholders.
Markets have a limited ability to look ahead. It's like a greedy algorithm. You're finding a local maximum, but not necessarily a global one (or even one that won't melt the planet).
The most efficient choice at any given moment (even incorporating a correctly priced carbon tax) may be to continue drilling. But due to the very long term capital investments, investing in drilling today because it's the best option, also guarantees it will be the best option tomorrow. So maybe additional interventions are required to reset the path dependence?
I think a purely market based solution would probably figure things out eventually, but we should also consider ways to help the transient response be as minimally disruptive as possible.
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.
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.
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!
>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.