> Today, we set out to formalize the entire Internal Revenue Code to hunt for unknown loopholes (bugs).

Saying that loopholes are bugs is a political statement that a particular allocation of resources is inherently fraudulent. There is no data that Lean code could use to decide whether a result is intentional or not.

It's like deciding that any tax provision that increases income inequality is illegitimate, and writing code to identify them. That could be a useful exercise, but it isn't a way to justify a human value with math. It may be a formalization of an ethic as applied to a tax code, but not of the tax code.

▲

whatshisface 2 hours ago | parent | next [-]

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.

	▲	bawolff an hour ago \| parent [-]
		I suppose, but most of the times loopholes aren't like that. Either they are intentional things that have unintended consequences or they are unintentional things that people didn't realize what they meant. Sometimes they are just laws that are working as intended but somebody doesn't like them so they are labelled as a loophole. I think there are very few loopholes that people intended to create by intentionally phrasing it weirdly.

▲

jamienk an hour ago | parent | prev | next [-]

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

▲

arjie 2 hours ago | parent | prev [-]

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.