[flagged]

Just in case your answers to the parent post's three questions were "Yes, yes and yes" here are some additional questions:

- Have you ever uploaded a container to Dockerhub or Quay.io?

- Does that container have an OS inside it that has user accounts?

- Before you answered parent post's questions, did it occur to you that you might have to update your Docker images to comply?

- Did you remember on your own that you also have to delete or update older Docker images to comply, or did you not think of that until you read this question?

After you've answered these questions, please re-answer the parent post's questions.

A lot of people people contributing to FOSS are volunteers. The calculus of working on stuff for free involves an assumption that your worst-case outcome is you make $0. This act's punitive fines change the worst-case outcome to somewhere around -$9999999 or more.

If you work on any programming project at all in any capacity:

- Are you confident your work doesn't fall afoul of this?

- Are you confident they won't decide to come after you anyway for insane political, bureaucratic or "seeing-like-a-state" dysfunctions?

- Are you willing to bet millions of dollars in potential fines that your answers to the previous two questions are correct?

Here's my suggestion for an implementation strategy:

- Keep the "Next" button greyed out until you add three forms of identification.

- Ask the user to take photos of their 3 forms of ID with a webcam. Ask the user to hold them in increasingly bizarre poses -- left hand, right hand, woven between your fingers, behind your ear, between your toes.

- Add an "accessibility" button. This button pops up a text box that advises you if you can't comply because you don't have hands, ears, feet or whatever (hey, some people don't and that's perfectly fine!) you can just use a picture of somebody else's body parts, and helpfully provides a menu of AI-generated pictures of human ears, hands, etc. for you to copy-paste.

- To preserve privacy, send the actual photos to /dev/null.

- The "verify the photo of my ID" button should check whether random.random() > 0.8. On average the user will require 5 tries per photo, or 15 tries total.

- Add a checkbox that says "I am not in the state of California". Upon clicking this checkbox the "Next" button becomes not grayed out and you can proceed without completing the identity checking process.

- If the user does not seem to have a webcam installed, all UI elements are grayed out except the "I am not in the state of California" checkbox.

- If the user is installing via command line, say "Are you in the state of California [y/n]?" If the answer does not start with 'N' or 'n', it will simply repeat the question.

- The list of acceptable identification shall be: Driver's license, learner's permit, Social Security card, library card, school identification, Boy / Girl Scout membership card, school yearbook photo, Burger King Kid's Club membership card, utility bill, ISP bill, Burger King receipt, Mahalo Rewards card, any receipt paid via credit card, birthday card, a photo of a printout of any email from OnlyFans, a photo of a DNS TXT record containing the string "CALIFORNIA", a photo of your X account with a blue check mark.

It seems like sound testing methodology to identify important theorems related to the code, prove them, and then verify the proof.

Verification gets sold as "bulletproof" but I'm skeptical for a couple reasons:

- How do you establish the relationship between the code and the theorem? Lean theorem can be applied to zlib implemented in Lean, what if you want to check zlib implemented in a normal programming language like C, JS, Zig, or whatever?

- How do you know the key properties mean what you think they mean? E.g. the theorem says "ZlibDecode.decompressSingle (ZlibEncode.compress data level) = .ok data" but it feels like it would be very easy to accidentally prove ∃ x s.t. decompress(compress(x)) == x while thinking you proved ∀ x, decompress(compress(x)) == x.

I've tried Lean and Coq and...I don't really like them. The proofs use specialized programming languages. And they seem deliberately designed to require you to use a context explorer to have any hope of understanding the proof at all. OTOH a normal unit test is written in a general purpose programming language (usually the same one as the program being tested), I'm much more comfortable checking that a Claude-written unit test does what I think it's doing than a Claude-written Lean proof of correctness.