Skip Navigation

InitialsDiceBearhttps://github.com/dicebear/dicebearhttps://creativecommons.org/publicdomain/zero/1.0/„Initials” (https://github.com/dicebear/dicebear) by „DiceBear”, licensed under „CC0 1.0” (https://creativecommons.org/publicdomain/zero/1.0/)B
Posts
3
Comments
876
Joined
2 yr. ago

  • 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.

  • What does “official budget” mean?

    A pre-plan for spending, generally involving an upper limit by category, including not only existing scheduled payments, but also ad-hoc spending.

    Like most plans, a budget can be as loose or a tight as you want, and you may or may not follow it, but just building it can result in a more successful approach.

    I think most people use a spreadsheet, so they can include some things that are auto-calculated, but that's not a essential property.

  • I'm 45 and I've spent more time on my diet (in the form of sodium and calorie budget(s)) than any sort of financial budget.

    That said, my vices are relatively inexpensive, my jobs have generally paid very well, and I do check my various accounts without being prompted.

    I think personal budgets (including my dieting) are best thought of as attempts to solve specific problems, not some sort of mandatory / expected behavior.

    If you are getting dinged with overdraft fees or CC interest etc., a budget might get you to a better place than you are on "just vibes".

  • I didn't see you link any of your sources, but I'll bite:

    https://pmc.ncbi.nlm.nih.gov/articles/PMC11882681/

    https://www.forensicscijournal.com/index.php/jfsr/article/view/jfsr-aid1068

    Also:

    For example, in 2006, the Roman Catholic Diocese of Dallas gave over a Eucharist host that turned red while in a glass for the analysis by two University of Dallas biology professors who concluded it was naturally explicable, as Bishop Charles Victor Grahmann wrote that "… the object is a combination of fungal mycelia and bacterial colonies that have been incubated within the aquatic environment of the glass during the four-week period in which it was stored in the open air.

    -- https://en.wikipedia.org/wiki/Eucharistic_miracle#Scientific_analysis_of_flesh_and_blood_miracles

    I got that off the first page of a DDG search (no AI) for: eucharistic miracles study nih

    Please do not reply. Or at least try to sound like less of a troll in any reply to me than in the rest of your posts in this thread.

  • So, if you get the lawyers involved, things could go very bad. BUT, I'll bet if you let enough labor lawyers read this, at least one of them will take the case under terms that you might want to accept.

    IANAL, TINLA, but I agree with the other posters that this could be a violation of federal regulations. (But, there's a lot of details I cannot glean from the posting that could affect legality.)

  • Sado

    Jump
  • If we have to cause suffering to survive...

  • I find it difficult to believe that this kidnapping is the only one in progress and also sufficiently more important (than the other kidnappings) to justify the additional news coverage.

    But, my heart does go out to her family and other loved ones.

  • Oracle is not the worse DB in existence. They are a worse company than MS, but I'd much rather be talking to Oracle than MSSQL.

    (My go-to is PostgreSQL, tho.)

  • Unfortuntely, nothing fine-grained enough for me. But, you can block communities and users (or even whole instances).

    I prefer the keyword filters on Mastodon, but I don't mind the political stuff, so my needs are clearly different from yours.

  • Definitely burning. It is possible to make reusable plastics out of oil, e.g.

    Of course, plastics might have their own problems, but they aren't always CO2 emissions.

    It seems unlikely we'll be able to completely eliminate plastics (current medical practices is the sticking point I see), tho we can certainly make a more "circular economy" around them, to reduce the need for oil extraction.

  • I only buy pizza from The Hut.

    See, this pizza comes with cheese in the crust; that's not normal, it's awesome!

    (Seriously tho, the Dominoes is closer, and if someone local was making the equivalent of "sutffed crust", I'd order from them. But, I'll pay a premium for cheese in the crust.)

    EDIT: TIL Dominos has a stuffed crust option as of May 2025, and Papa Murphy's might.

  • We should have nationwide consistency on who is eligible to vote (felons?) and how/when to register to vote (same day? automatic as part of getting state id?), yes. I think that's actually what his addled brain was thinking of, even if it's because he thinks blue states "cheat" at all states from rules-making to operations, which we have good evidence no state does, blue or red--other than gerrymandering.

    But, there's little need for it to be actually administered by the federal government (our state and local governments are corrupt enough). In fact, any election activities by the federal government should be more like FEMA, where they assist the states be the states remain in control from procedures to priorities and everything else.

    I wouldn't be opposed to UN election observers, either.

    I don't know if this it "the line", but I wouldn't expect anything less than state pd vs. national guard standoffs at voting locations in blue states, just like we had around schools during desegregation in ex-confederate states. Blue state governors are unlikely to stand down; they generally has good poll numbers / support.

    I'm in Arkansas so it won't matter if they nationalize or not; plus, Sanders will volunteer for nationalization of our voting operations and claim it saves money and benefits the people of Arkansas.

  • So far, everything I've wanted is freeleech, so that hasn't been an issue. I continue to seed, but the ratios are much worse for the same amount of time seeding.

  • I'm a BS in CS from UA Fayetteville. But, that was 20 years ago.

  • Programmer Humor @programming.dev

    Dev creates astrology-powered CPU scheduler for Linux, makes decisions based on planetary positions and zodiac signs — sched_ext framework informed by lunar phases, cosmic weather reports, and dynamic

    www.tomshardware.com /software/linux/dev-creates-astrology-powered-cpu-scheduler-for-linux-makes-decisions-based-on-planetary-positions-and-zodiac-signs-sched-ext-framework-informed-by-lunar-phases-cosmic-weather-reports-and-dynamic-time-slicing
  • Piracy: ꜱᴀɪʟ ᴛʜᴇ ʜɪɢʜ ꜱᴇᴀꜱ @lemmy.dbzer0.com

    Season Torrents

  • Comic Strips @lemmy.world

    Social - Saturday Morning Breakfast Cereal

    www.smbc-comics.com /comic/social-2