FoxQuirk 🦊 @quirk@computerfairi.es

A tagged subway car will always look better than one fresh from the factory. Why shouldn’t people in the city beautify their own trains? Why do we let them fill up with advertising instead?

If you're in Australia, Trans Justice is running a survey about access to and experiences with gender confirming health care, to provide data in support of their work pushing for better access. Seems designed to include DIY experiences, and those who want access but have yet to get any care. Open to all trans and gender diverse people in Australia
https://transjustice.org.au/survey/
#Trans #Australia #TransgenderHealthcare

girls only want one thing and it’s for mikrotik’s dhcpv6 to say “Status: bound”

got the bit-endianness of a bitmap format wrong again award

Yes I did transcribe alt text for this. My eyes hurt now.

Okay, we have a new contender for Most AI Thing to Ever Happen

1) July 25th: someone messes around with an LLM and posts a proof of the Collatz conjecture that does, in fact, verify in the theorem prover. (The AI use is not disclosed on the github page) https://github.com/xrchz/CollatzLean

2) July 26th: several serious bugs are posted in the theorem provers, that in principle could allow a false statement to be "proven" true. They're serious, yes, but no need for panic, because you're not going to blunder into accidentally exploiting the bugs while writing a proof, probably.
https://github.com/leanprover/lean-kernel-arena/pull/81

3) July 28th: someone who was right to be very skeptical of the Collatz proof, and had the expertise to study it with a fine-toothed comb, discovered it was exploiting a bug https://github.com/leanprover/lean4/issues/14576

4) The "proof" turns out to be exploiting multiple similar but distinct bugs to pass different solver variants!

5) the human who posted the proof acknowledges the AI use and claims they did not knowingly point it towards the bugs it exploited. https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Counterexample.20to.20the.20Lean.20Conjecture.20.28Soundness.20Bug.29/near/613135216

Note that the proof was posted shortly before the related bug reports were posted. It is an open question if the AI found people discussing the bugs shortly before they were formally posted and "decided" to exploit them, if the AI "knew about it" as a learned strategy from the training stage (putting every single "proof" it's ever made and ever will make into profound doubt), or if it's recently been repeatedly blundering into it by sheer stupidity and that's how people noticed the bug at about the same time.

Theorem provers aren't magic, and have bugs just like all other programs. They are tools to help us double-check our reasoning. When you skip the reasoning and ask an AI to "prove" something for you that's over your head, you're entering an adversarial pact with the monkey-pawed Devil of Customer Satisfaction.

my initial source for investigating this myself: https://lipn.info/@mevenlennonbertrand/116997927457012577

Ever wished you could have multiple independent mouse cursors on your Linux machine? No?

Anyway, turns out Wayland supports that pretty well! Let me tell you what I learned:

https://blinry.org/multi-seat-wayland/

“ah, no no, that factoid about Araragi-senpai is only established in a deuterocanonical work, I'm a Protestant”

this may as well be the Bible they're gonna be unearthing new Monogatari stories for centuries to come

reading the Japanese Wikipedia article there are how many Monogatari series short stories?!

Today, #Coreboot met #FreeBSD.

https://cgit.freebsd.org/src/commit/?id=5f74217c05a99f38a31a6e4950220964595d4ac8

When I started writing FreeBSD drivers, a friend told me:

So you’re just copying Linux drivers and rewriting them for FreeBSD ? Sounds like script work.

I explained that it doesnt work like that. First you understand the hardware. Sometimes you have to reverse engineer it. Then you test it. Only after that do you submit a driver.

He replied:

Fine. Then write a driver that doesn’t exist in any operating system.

That turned into a 500 MAD bet. (MAD is Morocco’s currency, not a measure of my sanity.)

The challenge is harder than it sounds. Almost every piece of hardware already has a Windows driver, a MacOS driver, a Linux driver, or follows a standard interface.

You dont invent hardware. You find a missing need.

So I wrote a driver for Coreboot.

Normally, the kernel log starts when the kernel boots. Everything that happened before that is a mystery. You can make educated guesses, but thats all they are.

With this driver, FreeBSD can read the Coreboot log. You get to see what happened from the very first moment the machine powered on.

That is exactly how I tracked down systems where RAM training was taking far too long because of defective memory chips.

None of this would have been possible without the amazing work of the Coreboot team.

As far as I know, FreeBSD is now the first operating system with this driver.

DragonFlyBSD is next.

Thanks to doordash building drones it will be the first time in history you can hunt a flying robot and collect food from the remains.

This behavior will be encouraged until morale improves.

I really like Procreate's Statement on AI. https://procreate.com/ai

#NoAI #AIPlague

left the house with the orb running and came back to this

it's actually way, way worse than I implied, and this isn't any kind of joke

You can get SIX computers for the price of a nice sub sandwich delivered to your door

going back in time and telling baby!Alice that one day, you'll be able to go online and order a computer 8 times faster than her packard bell, with dual cores, and it'll arrive within 24 hours.

and she'll also be able to do the same for a sandwich, and the sandwich will cost more

I dunno why there are so many OLED/LCD modules for the pi pico that use a nice header that cleanly fits over all the pins

so it's great if you want to easily connect a display, terrible if you need to connect it to LITERALLY ANYTHING ELSE

the pico has like 30 GPIO pins! your OLED is NOT using all 30 of them!

I just went and installed it on Win98 since Win3.1 was crashing every time

added basic enemy attacks to You Have Died (And Been Reincarnated As A Fox Girl), a game about being reincarnated as a fox girl in a dungeon town where everyone else is also isekaid girls and gay shenanigans and dungeon diving ensue