dwheeler

7 ms·

1.
by dwheeler 12d ago
Metamath is short, which does make it easier to verify. In addition, because it's simple, there are many implementions. The set.mm Metamath database, the most popular, is checked by 5 independently implemented proof verifiers.
2.
by dwheeler 24d ago
Another AI harness is Goose, which is OSS and housed under the Linux Foundation (LF) Agentic AI Foundation (AAIF): https://github.com/aaif-goose/goose Full disclosure: I work at the LF, but not the AAIF.
3.
by dwheeler 29d ago
Very cool. The metamath community tends to centralize results, so its equivalent is simply: https://us.metamath.org/
4.
by dwheeler 1mo ago
Most HUMANS will do anything to avoid learning from history. Engineers are merely an example. Sigh.
5.
by dwheeler 1mo ago
Yes, there's even a spec here: https://www.usb.org/sites/default/files/usb_type-c_cable_log... The cables are supposed to be labelled with their maximum speed (5, 10, 20, 40, or 80 Gbps or nothing if n
6.
by dwheeler 2mo ago
Metamath contributor here! Each proving tool has its pros and cons, but always happy to see Metamath noted :-). One thing that's cool about Metamath is that the axioms are not built-in. It's true that the most-used system is bas
7.
by dwheeler 2mo ago
I love this, and more generally the Triptych Project. We shouldn't need to use JavaScript to work around important limitations in HTML that are widely needed.
8.
by dwheeler 2mo ago
That beautiful is.
9.
by dwheeler 2mo ago
Wait a sec. My understanding is that passkeys are public/private keypairs. Public is in server, so even breaking into a server does not reveal the private key. The big risk with passkeys is storing the passkey where it will be held h
10.
by dwheeler 2mo ago
Impressive, but no castling or en passent, so it's not really chess.
11.
by dwheeler 2mo ago
Should be, but no.
12.
by dwheeler 2mo ago
Thanks! I strongly suggest copy-pasting that explanation to your web page, that's a nice summary.
13.
by dwheeler 3mo ago
I'm so glad I left LastPass a long time ago. There are better alternatives.
14.
Linux Foundation announces Akrites: coord/remediate/disclose OSS vulnerabilities(akrites.org)
8 points by dwheeler 3mo ago|0 comments
15.
by dwheeler 3mo ago
Perhaps, but I think volcanic eruption followed by system collapse is very compelling. Here is the story I find most convincing from the experts whose works I have read. It likely started with a volcanic eruption, leading to widespread fami
16.
by dwheeler 3mo ago
Horrible. Brilliant. Love it.
17.
by dwheeler 4mo ago
Thanks for the credit, I appreciate it! Glad it was helpful. I wouldn't call it a "blog post" though, it's simply an essay. I update my essay whenever I decide it needs updating, and "blog posts" are usually ch
18.
by dwheeler 4mo ago
Those interested in this might also like my "Project Hail Mary Stellar Map" at: https://dwheeler.com/essays/project-hail-mary-map.html My page shows a stellar map (from the viewpoint of Polaris) and a sky cha
19.
by dwheeler 4mo ago
Gnome Console seems to be intended for people who don't use terminals. I quickly install GNOME terminal for real use.
20.
by dwheeler 5mo ago
No, there is no reason to believe it can be enforced. In the US, training is considered fair use at this time, and thus DOES NOT require a license at all. That might change, but I doubt it.
21.
by dwheeler 5mo ago
I would say "limited and unreliable access". What it says is the cause might be the cause, but it's not on any way certain.
22.
by dwheeler 5mo ago
I think Inform 7 is pretty cool. I suggest checking in to that as well.
23.
by dwheeler 5mo ago
No. And training is currently considered fair use in the US (some court cases pending). I am not a lawyer, tho.
24.
by dwheeler 5mo ago
I suspect this is really a surveillance bill, but we won't know until the text is revealed.
25.
by dwheeler 5mo ago
I suggest this vocal performance: https://youtube.com/watch?v=GggK9SjJpuQ
26.
by dwheeler 7mo ago
I prefer the term "assistant". It can do some tasks, but today's AI often needs human guidance for good results.
27.
by dwheeler 7mo ago
I also made a list of tips on writing code with AI, with a special focus on security. Others may find the tips useful. Here they are: https://openssf.org/blog/2026/01/05/ai-software-development-...
28.
by dwheeler 9mo ago
This has many similarities to the Heartbleed vulnerability: it involves trusting lengths from an attacker, leading to unauthorized revelation of data.
29.
by dwheeler 9mo ago
Many people use Octave https://octave.org/ which is compatible (generally) with Matlab, supports this simple syntax, and is open source software. Indeed, I've taken at least one class where the instructor asked people
30.
by dwheeler 10mo ago
That's only true if future improvements are easy to create as past ones, that customers care as much about those improvements, and there are no other differentiators. For example, many companies do well by selling a less capable but mo

More ›