I’m also on Mastodon as https://hachyderm.io/@BoydStephenSmithJr .
If someone wants to collab, I’ve been writing various codes around it: https://gitlab.com/bss03/grtt
Right now, it’s a bunch of crap. But, it’s published, and I occasionally try to improve it.
Also, Granule and Gerty are actual working implementations, tho I think some of the “magic” is in the right grading ring for the runtime, and they and more research oriented, allowing for fairly arbitrary grading rings.
On my 45th, instead of a colonoscopy, my Dr. had me do the “Cologuard” stuff. Insurance covered that. I turn 46 this year.
The whole industry needs rebuilt from the foundations. GRTT with a grading ring that tightly controls resources (including, but not limited to RAM) as the fundamental calculus, instead of whatever JS happens to stick to the Chome codebase and machine codes spewed by your favorite C compiler.
I saw it 3 times opening weekend.
This deserves every upvote the top-level post got.
Neither vim nor neovim are safe! (I hear emacs is fine, but who really knows all the people that provided contributions to the pile of elisp they call their emacs.)
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”.
Yes, you can get the 100% juice label by taking (e.g.) cranberry concentrate and the reconstituting using (e.g.) apple juice instead of water, adding calories and sweetness without adding a (non-juice) sweetener.
On top of that, most of the juice aisle does not even qualify for the “100% juice” label.
Gotta read the fine print on the label AND the government labeling regulations AND have some level of trust in the government to get what you want from a mass-market product. Local products and producers are not a panacea either.
But, I’m going to overdose on ACE-K given the amount of Zero Sugar Mtn. Dew I think, so I’m not going to shame anyone for their favorite juice, whether it is “100% juice” or not, from concentrate or not, or whatever.
Fidelity, Banks, Coinbase (before I got out of cryptocurrency entirely).
But, basically, only when government regulation does (or SHOULD) impose KYC requirements.
Age and ID verification might be good in a very few cases, but it should definitely be a deviation from the norm.
I’m confused, why would “Accurate Noon” be important?
Why is any particular time important? It serves me to be able to tell time without a clock and synchronize my internal clock with solar activity.
And for countries that sit far enough from the equator, wouldn’t it be inaccurate regardless?
No. Distance from the equator doesn’t significantly affect when the sun it at it’s peak. It does affect how high in the sky the peak is.
Time adjustments (like “daylight saving”) drags the Sun E/W (which is why we “need” timezones). Increasing latitude dags the Sun N/S.
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.
RCV / a Condorcet Method might help.
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.
Honestly, I should get more comfortable with it.
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.
Sorry. I didn’t pick the acronym, it comes from the paper: https://arxiv.org/pdf/2010.13163.pdf I’m not sure why there’s no “M” in the acronym, but I should probably spell things out when I actually want collaborators.
While I’m dropping links, I will also drop https://github.com/granule-project/ where Gerty and Granule live and where real research is done.