In theory "impossibility" is a defense to most crimes.

In practice you usually get screwed in one of the following ways: a) the law makes it impossible to do X without breaking the law, even though X is a normal thing and neither law was supposed to be a total ban on X, but you could comply by not doing X at all, b) the inconsistent laws are imposed by different jurisdictions and then they each insist you follow theirs, often a special case of the first one where X is "be in two different jurisdictions" but sometimes the even stupider one where a jurisdiction demands that you follow its laws even when you're not in it, c) it's impossible for you to follow both laws at once so you followed only one of them and then they decide after the fact that you should have followed only the other one.

What are the books in particular? I liked Accelerando and was intrigued by the reputation markets mentioned.

> punishes married couples filing jointly: a couple making about $300K each

The number of married couples where each partner is making $300K each is a very, very small percentage of the population. Not sure this is a big deal to be concerned about in the grand scheme of things. For instance, only a few %age of households have an income over 300K in the first place, much less coming from 2 earners of that amount.

The tax code has significantly punished dual-income married couples for quite a while. It presumably started some time in the 20th century as some sexists not wanting women in the workplace and then continued because changing it to have them pay the same taxes as they would if they were unmarried would result in a significant reduction in government revenue.

Thank you for posting this!

Any change to the law that bill authors have to hide by phrasing the bill so that it sounds like the change is otherwise is illegitimate, and that's what formalization is meant to catch.

But some of the "bugs" do seem to be weird complex misalignments rather than directed tactics.

Agreed. In fact, you'll see things termed loopholes vs. benefits depending entirely on politics so it can't be a property of the law itself. An EV tax credit or SALT deduction are "loopholes" too.

I've heard this repeated a couple times here on HN. Do you have any citations for laws being vague on purpose? The whole point of laws, and the formal structure they take, is to reduce vagueness. Is this rock on person A's land or person B's land? When it turns out, despite best efforts, that a law is vague we even have a second system to step in and reduce the vagueness further: case law. I have no doubt that people are trying to exploit vagueness on both sides, but naysaying here is nonsense. And almost nobody wants law to be vague either.

> And also, it's important to remember that in tax matters, the final arbiter of interpretation is a judge. Judges are humans, not machines. You can't "Trick" them by saying "well technically this is allowed!". Because they rule on the sprit of the law, not as it was written. Judges aren't amused when you try to be cute with how you interpret a law. And some Judges have biases, where you get a different ruling depending on if you play at their golf club or not.

> Laws aren't computer code. They are vague on purpose.

Yes... but. Tax law is a bit different because it is similar to an equation: you put in your inputs and you get your outputs.

There have been famous cases where the courts have said in essence, "yes you completely and exactly and precisely followed the law, but we're not going to allow you to do that anyway." Those rulings have become less frequent.

This is ridiculous - first of all you don’t have to be rich to afford a CPA, second of all high earners almost always pay the highest rates (both effective and marginal). And even in the cases where they don’t pay huge marginal rates (dividends and LTCG), they don’t need a CPA to take advantage of that because it’s dead simple.

https://taxfoundation.org/data/all/federal/latest-federal-in...

> Because they rule on the sprit of the law, not as it was written.

I feel like this attitude is responsible for the modern destruction of the rule of law.

It doesn't matter what the law says, the only thing that matters is vibes! And whether you play golf with the right government officials.

> You can't "Trick" them by saying "well technically this is allowed!".

The obvious problem being that sometimes it is allowed. And then do you want that being decided by democratically elected representatives and specified ahead of time so the public can know what's expected of them and of others, or decided ex post facto on the basis of feels and discrimination?

> Because they rule on the sprit of the law, not as it was written.

Extremely funny to say that about US law when it is entirely based on precedent, and a single judge having vibes on a particular day changes how your entire country works for the next 50 years.

US law is explicitly made to be skirted, as is every common law system in the world and they are all irrevocably flawed.

I assume you'd want to prove common-sense invariants, like "you can't be taxed more than your income" or "tax credit 123-45 is worth more for two children than for one". Lean might disprove a few of these, and the counterexamples are potential loopholes.

Maybe tax change impact analysis by congress can easily be calculated using Lean. The article also said loopholes can be easily identified?

Maybe you could validate stuff, like "how much would I be taxed if I did X" and then have it come up with all the questions that need to be answered to determine the answer or "what's the max I could be taxed if I did Y"?

I don't know much about Lean, but I assume that beyond proving things it functions as a truth graph you could walk to calculate things...

Edit, it might also be (someday) useful when drafting tax law to make sure the law is actually sound (e.g. isn't contradicting something else) or to see what it's overlapping with?

You wouldn’t be proving the tax code, you’re proving that a procedure follows the tax code. This way you’d be able to know for certain if an AI that tried reducing your taxes actually gives you a valid procedure/result, assuming you can trust the Lean formalization (hint: you can’t given the nature of law, especially if it’s vibe coded like this)

this is actually a really bad idea and is the opposite of what a powerful state would want