alt Hacker News> 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.
Replies
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.
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.