There's nothing about prove2me that couldn't have been coded just like any other huge coding project frontier models have proven themselves extremely good at doing. It just happened to have been made by humans.
2,485 karma · joined April 23, 2019
HackerSmacker profile: https://www.hackersmacker.org/user/logicprog?hs=FFrqctXUcBYFlcykFq
Yeah, because before now there's been literally zero proof of an automated theorem prover scaffold around the LLMs being used, and big counterexamples and such being found, with raw chat logs available, where no such thing was used.
> Now they have it in writing.
Yeah, because now it's actually being done. They talk about it as a novel thing, because it is. You don't get to claim being "right all along" from this
My second point is that the models are way better at things like Rust or Lua than Python or JS, because the average person producing code in those languages has way more programming experience"
https://github.com/alexispurslane/cursed/
https://github.com/alexispurslane/industrialworld/
Feel free to look at my past projects, prior to me starting to use AI (which started with gemini-ocr) to assess my baseline skill level.
Also, what would be highly unusual to you?
For instance, a game engine written entirely in LuaJIT, but allocating almost all data structures using CFFI, a very unusual, custom object-orientation DSL I designed myself, and that uses SDL3's SDL_gpu library to do all rendering, a ton of GLSL 4.6 compute shaders cross compiled to SPIR-V and Metal (which constraints what GLSL can be written), and is a hybrid tile-oriented and 3D engine.
Another example is my Emacs-like live-modifiable image-based editor, again in LuaJIT+CFFI, with a kqueue+atomic lock-free ring buffer+pthread based actor model, each running a separate LuaJIT interpreter, with a custom advicing system, event bus, async/await implementation riding on the event bus, a custom process management and IO library, and testing via Tmux.
Even DeepSeek V4 Flash mostly does fine with this, once it's built a few memories in the memory system. Let alone something like DSv4-Pro or GLM 5.2. All I can say is skill issue.
Additionally, I quoted Tridge in response to a comment about an increase in changes to rsync, not in response to the person pointing at one bug Claude introduced. If you actually looked at the thread, you'd see that. I didn't deny the Claude introduced bug at all.
Thus, if anything their sev/10c is inflated. If I changed it to lines of code changed, the relative bug ratios would be much smaller, and the conclusion wouldn't change. In fact, the conclusion would look "better" for Claude; if I was using "mental gymnastics" to come to this conclusion, I would have already used a metric other than adjusting per commits!
What different metric would you suggest that would change the conclusion?
Showing "humility", as you so moralistically and condescendingly put it, would require being wrong first.
And once it's originally posted, it doesn't matter the great extent I go to address metrics and methodological critiques in order to ensure that the data is as robust and helpful as possible. And the effort in writing and refining my prose and the organization of the report in response to people's complaints and criticisms because I do value their time. And when people told me the AI prose was bad, I spent two hours to to make sure that it was something people would want to read, that doesn't matter at all? It's only the original intention that matters. So you just have this arbitrary cutoff point for what counts towards my intentions in the post and my character. No allowance for learning or adaptation, and the fact that I'm clearly committed to putting a lot of effort into making this something that is useful and pleasant to read for people, I just didn't do it for the first draft originally, doesn't matter, only the original version matters?
And more than that, you're not going to actually deal with the substance of the issue, the actual calculations and methodology and conclusions that I came to, instead, the only semi-substantive critique you're going to make of the post is to tone police me and dance around the real issues, as if you're afraid of ever touching them?
The best argument you could make that my bias actually influenced my conclusions would be to point into the methodology and metrics where I did that. I made it all extremely open and transparent and auditable both by describing it in extreme detail in the post and by providing all of my source code and the ability to build the database it runs on from scratch. If there was an actual flaw or bias that my intentions going into this created your biggest possible Smackdown, your best weapon in your arsenal would be to actually point that out. But instead, again, you're just tone policing me. but a polemical style in the presentation of an objective statistical analysis does not in the least undercut its accuracy. Have you considered that my polemic became so fiery, in fact, precisely because I ran the tests and found how non-existent the evidence was for this outrage and that's what made me angry? No, you didn't because you saw some words that hurt your feelings and now you won't listen to facts.
Why wouldn't it be except question begging priors assuming it couldn't be?
> Why does v3.4.2 have 0 bugs, or 0 bug score. And why was such an outlier (no other commit seemingly has this??) allowed to mix into aggregate statistics and bring all the "is Claude buggy?" scores down.
My original metrics which didn't filter out feature requests and questions had it at four bugs and prior to that it was even higher and it didn't make much of a difference to the overall analysis (fell well within the IQR, the lower end of it too). Also, removing one outlier just because it looks kind of funny to you, especially when we only have two Claude releases at all, would be worse in my opinion and more arbitrary.
"Like many developers of open source packages I’ve been hit by a flood of security reports lately in my role as the rsync maintainer. Many of those reports are AI generated (not all though, there are some notable ones with very careful and high quality manual analysis).
As this flood started to get more intense I realised I needed to raise the defences on rsync a lot — we needed much more thorough test suites, code coverage analysis, CI testing on a lot more platforms, deliberate and thorough scanning for possible security issues (so I find at least some of them before other people!) and the addition of a whole lot of defence-in-depth hardening techniques. This is all a huge amount of work. "
> This statement is honestly so ridiculous that I felt it didn't warrant a direct response, but here's one anyway: AI enthusiasts have been proudly proclaiming for literal years that AI makes them 10x as productive based on cherry-picked anecdotes with zero empirical evidence to back it up.
Let's go back to remedial classes on this one.
"I have found that [tool] has made me more effective" is what we call lived experience. It is an "i" statement communicating something about the person’s life. It does not require evidence by default, and you are a crazy person if you call bullshit without good reason, because many "I" statements are epistemically justified in ways that can't be empirically demonstrated or require tacit knowledge.
"[tool] has been buggier since [change]" is a falsifiable claim; you need to actually provide evidence for believing it, and what I'm showing is literally that there isn't any.
I'm talking about the double standard on the anti-AI side about what evidence should count, not some vague industry-wide epistemic standard, whatever that means. I'm aware LinkedIn Lunatics and Steve Yegge are also being crazy. And it seems to me that even your response here is engaging in a bit of a double standard, or something akin to it, in that you think the irrational anti-AI behavior should be given a pass — and the conclusions perhaps even taken seriously — just because pro-AI people did it too.
> And that doesn't help. If anything, editing the AI output to make it read less like blatant slop just comes off as deceptive, like you're trying to hide the fact that the analysis was AI generated.
Okay, so, if I don't spend the time to write everything myself, that's bad because it's AI slop. If I do rewrite everything myself, then it's evidence of deceptiveness... despite being asked by multiple people to do that, and being extremely explicit about my methods and process and the commit history being (as you've shown), very public.
Also, the AI-generatedness of the text doesn't mean the analysis is AI generated, in terms of what was actually done. That's a category error.
> Looking at the commits, you were adding more AI generated text less than 2 hours ago[0] before quickly editing out one of the most blatantly sloppy sentences I've ever read[1].
The second commit literally says that that was my prose it was fucking with by adding slop. It's just that me adding my prose, and it adding slop to it, were in the same previous commit. Additionally, my process is often giving it exactly what I want to say, more or less, and having it HTML-format it and insert the templated numbers and UI widgets around that text.
But again, even if I'm spending the time to read through and edit everything it's writing to de-slop it, then I'm clearly also reading it through enough to make sure the analysis makes sense, and is accurate; how is that not enough "effort" for you, if effort is supposed to be a proxy for verification?
> Even if we ignore the bias clearly on display there, the premise alone is enough to dismiss the entire thing as heavily biased and chasing a pre-determined conclusion - of course someone who is so dependent and trustful of AI that they decide such an analysis on the bugginess of AI code should itself be written by AI is going to steer the conclusion towards "actually AI code is good and you luddites are overreacting".
That's not ignoring the bias, that's literally restating that you think the bias is there. But if you really think that my bias meaningfully "steered the results," then show me how that happened. Tell me how you would've proven the Claude releases were meaningfully worse, or unusual, at all, or how the methods I chose biased the data against that result, or literally anything except shifting the goalposts and using accusations of "bias" as a get-out-of-jail-free-card.
> The entire concept is so tone-deaf that failing to notice it or predict the criticism before publishing is enough to prove the bias.
And you're so committed to your preconceived notions that anything made with AI must be bad, wrong, or not worth your time, that you'll spend your entire time begging the question ("it's made with AI, therefore it's wrong") and shifting the goalposts instead of engaging meaningfully.
Also, I certainly predicted the criticism (in general, anyway, to the fact that it was made with AI; not the prose being AI) but I made it this way anyway, because if someone is so AI-blinded that they can't read and evaluate the actual metrics, methodology, and provide meaningful criticism to it, and instead can only see that it was made with AI, and they're so it doesn't matter.
Nothing you have said makes the analysis wrong. At this point, you're essentially just resorting to ad homenem and begging the question.