I was a professional, and I didn't have a backup of my personal system for about 2 decades. I just didn't have another 4TiB of storage to copy my media library onto. I'm now on backblaze, but there was a long time there when I did not have a backup even tho I knew better.
Also, even in a professional setting, I've seen plenty of "production support" systems that didn't have a backup because they grew ad-hoc, weren't the "core business", and no one both recognized and spoke up about how important they were until after some outage. There's virtually never a test-restore schedule with such systems, so the backups are always somewhat suspect anyway.
It's very easy to find you (or your organization) without a backup, even if you "know better".
I'd rather have accurate noon / celestial time for the few months it is still allowed and still have to switch twice a year than let the government make wrong-noon ("daylight saving") time permanent. So, many of the "end time switching" movements I actively resist rather than support.
I imagine things like this aren't "done and over" because there is no majority opinion.
Investment as a form of collaboration and results distribution is probably fine. Tho, I would not be opposed to limits on size/scale for companies, individual wealth, pay ratios, etc.
Shorts, options, and other "exotic financial instruments" are worse than gambling because they compel corrupting (withering) behavior.
I think an active, forceful SEC based by a similarly aggressive DOJ, both focused on benefit-to-working-class primarily and market-health (e.g. lack of rent seeking, monopolistic, or monosoponistic behavior) secondarily, would lead toward a better (for global society) market. I think that could be true even if we continued to allow fairly arbitrary contracts that are those "exotic financial instruments", options, and shorts.
I agree that gene editing to reduce suffering is good. I'm not sure "designer babies" is a label that includes those gene edits. Or, if it does, it groups the with too many other gene edits so the good ones are no longer exemplary of the label.
I think the knock-on effect of making some innate, human characteristics undesirable is probably a net bad. That's very close to labeling persons with those characteristics as sub-human--specifically due fewer "human" rights.
That said, if I were choosing between gametes or embryos and had genetic information on them available, I do not think it is a moral stance to ignore/discard that information when making the choice. We should be careful to understand our genetic knowledge is still quite limited and, even if our knowledge was perfect, (most) genotypes are not destiny.
Also, my preference shouldn't matter to anyone else. If you want to increase your proof assistant skill (even from nothing), I suggest lean. Probably the same if you want to increase programming skill in a dependently typed language.
Right now, I'm spending more time in Idris. It's not a great proof assistant, but I think it's a lot easier to write programs in. Rocq is the real proof assistant I've used, but I don't have a strong opinion on them because all the proofs I've wanted/needed to write where small enough to need minimal assistance. (The bare bones features that are in Agda or Idris were enough.)
Yes, I've written some Lean. It's not my favorite programming language or proof assistant, but it seems to have "captured the zeitgeist" and has an actively growing ecosystem.
Yeah, software is already not as deterministic as I'd like. I've encountered several bugs in my career where erroneous behavior would only show up if uninitialized memory happened to have "the wrong" values -- not zero values, and not the fences that the debugger might try to use. And, mocking or stubbing remote API calls is another way replicable behavior evades realization.
Having "AI" make a control flow decision is just insane. Especially even the most sophisticated LLMs are just not fit to task.
What we need is more proved-correct programs via some marriage of proof assistants and CompCert (or another verified compiler pipeline), not more vague specifications and ad-hoc implementations that happen to escape into production.
But, I'm very biased (I'm sure "AI" has "stolen" my IP, and "AI" is coming for my (programming) job(s).), and quite unimpressed with the "AI" models I've interacted with especially in areas I'm an expert in, but also in areas where I'm not an expert for am very interested and capable of doing any sort of critical verification.
I was a professional, and I didn't have a backup of my personal system for about 2 decades. I just didn't have another 4TiB of storage to copy my media library onto. I'm now on backblaze, but there was a long time there when I did not have a backup even tho I knew better.
Also, even in a professional setting, I've seen plenty of "production support" systems that didn't have a backup because they grew ad-hoc, weren't the "core business", and no one both recognized and spoke up about how important they were until after some outage. There's virtually never a test-restore schedule with such systems, so the backups are always somewhat suspect anyway.
It's very easy to find you (or your organization) without a backup, even if you "know better".