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

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.