←back to thread

Catala – Law to Code

(catala-lang.org)
116 points Grognak | 1 comments | 06 Dec 25 22:11 UTC | HN request time: 0.001s | source
Show context
sublinear ◴[07 Dec 25 00:32 UTC] No.46178080[source]▶
> The aim is not to formalise or put into code all the law, because that would make no sense, but we are interested in the law that is already executed automatically, such as the calculation of social benefits, tax or unemployment.

Can anyone explain why it's believed this "would make no sense"?

replies(8): >>46178118 #>>46178209 #>>46178320 #>>46178385 #>>46178481 #>>46179102 #>>46179190 #>>46179304 #
1. solidsnack9000 ◴[07 Dec 25 05:06 UTC] No.46179304[source]▶
It does stand to reason that all law could be formalized. For example, consider the definition of murder in the first degree from 18 USC § 1111:

"Murder is the unlawful killing of a human being with malice aforethought."

You might say, well, "unlawful" and "malice" are fuzzy concepts; but we can take them to be facts that we input into the model. I guess we could write something like this in Catala:

    scope Murder :
      definition in_the_1st_degree
        under condition is_malice_aforethought and is_unlawful consequence
      equals
        true
In the calculation of social benefits and taxes, the facts input to the model are generally things like prices, depreciations, costs, areas of offices, percentages and so on, input numerically and sworn to be true. These numbers are then used to calculate an amount due (or in arrears). Performing the calculation in a way that is verified to conform to the law is a big part of the work.

However, in other areas of law, determining the facts is actually where the real work is -- was there malice aforethought? A formalized legal machine could process these facts but it's not a big help. The models would just be a huge list of assumptions that have to be input and a minimal calculation that produces `true` or one of the alternatives of an enum.