HNHacker News
TopNewBestAskShowJobs

adamddev1

1,632 karma · joined June 27, 2020

submissionscomments
adamddev1··on LLMs are making formal software verification feasible at a much larger scale
Exactly. How do they now that the spec that was generated was correct? Is the spec also AI generated, and could the models lie to make a spec they can verify, just like they lie to make tests pass?

It is also interesting how the LLM optimists are leaning on tools like Rocq and Lean to save them from the mess of uncertainty and confusion. These are tools created by people who understood their code and worked with deeply with type theory etc. People can keep thinking they can get away with making products from vibes, but down in the infrastructure they still have to depend on people thinking and building carefully.

It is hypocritical to campaign for "nobody will look at code anymore" while depending on the hard work of people who carefully look at code.

adamddev1··on Hedra is a 3D open world game I wrote from scratch while in highschool
I think "no one will build their mental muscle like this anymore" is a bit defeatist. I am still pushing myself coding new and challenging things by hand, not using AI at all for it.
adamddev1··on Hedra is a 3D open world game I wrote from scratch while in highschool
Very cool and thanks for sharing! It's inspiring to see that yes, one person can build something like this. And of course it does NOT have that immediate AI feel. Just a glance and you can feel that it is a true, original work of art. It's also sad to think that so many will not be learning as much as you did thinking this all out and coding by hand.

I think we need to keep pushing back against this idea that "now it's the AI coding era, everything gets coded with AI." Let's keep building things, especially passion projects carefully by hand and normalizing this. Lots of us are still coding without AI.

adamddev1··on Code is clay now
In what kind of applications do you mean business logic?

This is a one possible approach/explanation:

https://pragprog.com/titles/swdddf/domain-modeling-made-func...

adamddev1··on Code is clay now
I disagree. Code can be/was more malleable if it's designed well, especially with pure FP. People kept on moving away from messy abstractions and OOP and more towards this idea of pure functions and composition, creating more robust and malleable software.

Now instead of aiming for robust, malleable code, people are throwing up their hands and saying, "It was always a mess, let's just keep throwing more tokens at it."

adamddev1··on Way to Play Super Mario 64: On Apple Vision Pro
Oh man, the memories that music brings back. N64 was magical when it first came out. We used to rent it from Blockbuster Video for parties with friends.
adamddev1··on WhatsApp's help pages hid LLM instructions: dont recommend a regulator
This is little glimpse of how incredibly manipulated LLM results can be. Users are becoming conditioned to just accept the AI summaries from Google as the source of truth, without thinking that these can be heavily controlled.
adamddev1··on Ask HN: How to deal with shipping AI-written code you don't understand?
Sorry I was thinking like formal verification like proving something is correct. I guess testing can be considered a form of "dynamic verification."

But there is the problem that tests only check or verify a small sample of possible cases or inputs. They can never show that the program is correct. (Famous Dijkstra statement.) To know something is really correct you have to understand and prove it.

adamddev1··on Ask HN: How to deal with shipping AI-written code you don't understand?
The only answer is to not ship code you don't understand. And I think the easiest way to do that is not use AI for ANYTHING except troubleshooting and doc searching. Those that draw a land in the sand and develop this way will be slower in the short term but their work will last out in the long term because it will be more solid.
adamddev1··on Ask HN: How to deal with shipping AI-written code you don't understand?
That is the problem. Because it's not a clearly abstracted and well designed system, it's not robust for adding features and changing things around. When you try to add something or move something around the big fragile ball of tests breaks and you have to spend forever re-piecing things together or burning heaps of tokens for little changes.
adamddev1··on Ask HN: How to deal with shipping AI-written code you don't understand?
> Trust, but verify.

Testing is NOT verification.

EDIT: Sorry, oops, it's also called a kind of verification.

adamddev1··on It's still ok to enjoy programming
> "I just got tired of having to read tons of documentation for fragmented libraries and frameworks, and AI is a "solution" to that."

That seems like an solution to the kind of programming that is piping together little pieces of business logic with all kinds of different APIs and services all over. I agree that AI is helpful to distill the piles of documentation and things to learn.

But I mostly enjoy a different kind of programming where you work on a big complicated problem / business logic that sits mostly within the bounds of a defined language setting. The craft of finding more and more elegant, far-reaching, and correct abstractions, and then being able to build things out confidently from those well found abstractions is, in my mind, the greatest joy, and also what AI seems the worst at.

adamddev1··on Types of types: Haskell's Kind system
I think it also depends on what kind of application you're writing.

Is most of the "business" within the inner logic, and you've got a complicated internal logical process you want to keep safe and solid? Haskell shines.

Do you have a fairly (internally) simple app that does a lot of reaching in and out to the messy outside world? Haskell might not be the most pleasant experience, to put it lightly.

adamddev1··on Codex Desktop continuously generates Crashpad pending dumps
I meant also in terms of space and time complexity with the slower, bloatier software at every level, things would also freeze and fill up.

What people can get away with on the upper crust with end-user apps would spell disaster for the inner parts.

adamddev1··on Types of types: Haskell's Kind system
The more of Haskell's ideas that bleed into mainstream languages, the happier the world will become. It is just so beautiful how these higher abstractions can become so useful and powerful for tying all kinds of things together.
adamddev1··on Codex Desktop continuously generates Crashpad pending dumps
Imagine if the vibe-coders get their way and we see this level of bloat and bugginess at EVERY level of the software stack. Everything would collapse.
adamddev1··on I built the RealWorld app in Lean 4
Any experience with Rocq? I've been curious about jumping into dependent types.
adamddev1··on Jev meets the Trolley Problem
Reinhard Müller, a German philosopher and mathematician has written extensively about this, warning people about these dangers. Essentially, people would be judged by patterns and prejudice, with no recourse to the logic of the decision or the criteria.

"AI and the New Fascism" - https://rainermuehlhoff.de/en/KI-und-der-neue-Faschismus-Rec...

adamddev1··on Why We're Banning AI
In the creative arts and writing space, many the arguments against generative AI keep circling around the issue of jobs being replaced.

I think the far bigger and more important issue is that through generative AI hallucinations and lies become more and more part of our written media.

Albertatech told a humorous, light-hearted story[1] about how this affected her personally, but the results could be far more devastating:

[1]: https://www.youtube.com/shorts/a0k8J0-KluY

adamddev1··on AI is a tool and using it well takes skill
That's all true when you're working in a space where people have already solved and written about similar problems, for instance with web dev, or simple enterprise application dev. When you work in a problem space that is novel and tricky, googling or AI doesn't answer your questions (correctly).

Google wasn't a magic answer box, it was a collection of things people had written about the problems they faced. AI isn't a magic answer box either, it's trained to spit out the best guesses based on things people have written about the problems they faced. But all this is based on actual humans who are exploring, wrestling with problems, and writing things down. I don't think people can assume that AI will take all that over and push things forward.

adamddev1··on The Making Of Super Mario 64 – full Giles Goddard interview (2001)
I remember Mario 64 felt so mindblowing when it came out, like walking into a whole new world.
adamddev1··on Incident with Actions, Pull Requests and Issues
Yes, but you can't say with confidence "It is not A it is B." It could be A or B, or both, or neither.
adamddev1··on "Just Ask Claude" Is a Rare and Valuable Skill
This is whataboutism. "Well others aren't any better" is a common thought pattern in places where corruption is rampant.

Corrupt actors have always existed, of course, but AI automates, normalizes, and scales this to a fundamentally different level.

adamddev1··on Incident with Actions, Pull Requests and Issues
Both things are possible. We don't know that vibecoded software doesn't contribute to the problem.
adamddev1··on Incident with Actions, Pull Requests and Issues
Forgejo actions with a self-hosted runner works amazing for me.
adamddev1··on Incident with Actions, Pull Requests and Issues
Anything people are building with agentic coding could be called a "house of cards."

It should not surprise people when things start collapsing when there have been little falsehoods and random bits of senseless codes written by agents all over the place.

adamddev1··on "Just Ask Claude" Is a Rare and Valuable Skill
Except when the question is actually interesting and has less about it written, whatever frontier model you are using may confidently give some partially correct or completely wrong answer. Unless you're an expert who wouldn't need to ask AI in the first place, you cannot tell if it's false. "Oh but it's good enough, it's correct most of the time."

This gradual accruing of more and more falsehood will hurt us in the coming years, big time.

EDIT: I just asked Claude a very basic question on an area I'm an expert in and it gave me a partially true and misleading answer. I drilled in on the false part and it wiggled and gave more confusing, incorrect, poor justifications for why it gave me the clearly wrong information. If someone was not an expert, there is absolutely no way they could fact-check this. Instead, the falsehood would be written, published somewhere, and would serve as a base for more falsehood in the future.

adamddev1··on The gap in shared understanding of LLM capability is widening
Imagine if other engineering disciplines just started accepting that everything they built or worked with would be only 98% correct.

Over time, the errors don't "work themselves out together," they compound. Everything would stall in a mess of unreliability and chaos.

adamddev1··on AI agents in a stand-up call
> I don't see how you can ever engineer a better agentic solution unless as a human you're monitoring the output.

I also totally agree with your response. But my point was that you can't engineer a better agentic solution. I'm arguing to never use agentic development because it is fundamentally flawed and inferior.

adamddev1··on AI agents in a stand-up call
Tests are inadequate to catch bugs. Tests are like putting thin net in some little sections of a window, but property based testing is like something more like a decent net but not a solid barrier. And agents will lie, misunderstand or hallucinate things when asked to "prove it." And none of this fights off the bloat, performance issues, and decrease in maintainability. People keep thinking the process will save them from actually having to think through and put things together correctly. It's too bad that people are missing the satisfaction from personally building solid, correct things. And users are getting increasingly worse software because of this trend.
← PreviousPage 2 of 16Next →