There's really no such thing as complete verification.
The quest for purity is some fountain of youth nonsense that distracts a lot of otherwise brilliant engineers.
Ask the AI to make a program that consumes a program and determine if it halts.
Readit Newsjappgar commented on AI will make formal verification go mainstream martin.kleppmann.com/2025... · Posted by u/evankhoury
jappgar commented on AI will make formal verification go mainstream martin.kleppmann.com/2025... · Posted by u/evankhoury
> In my experience, the more information is encoded in the type system, the more effort is required to change code.
I would tend to disagree. All that information encoded in the type system makes explicit what is needed in any case and is otherwise only carried informally in peoples' heads by convention. Maybe in some poorly updated doc or code comment where nobody finds it. Making it explicit and compiler-enforced is a good thing. It might feel like a burden at first, but you're otherwise just closing your eyes and ignoring what can end up important. Changed assumptions are immediately visible. Formal verification just pushes the boundary of that.
It is definitely harder to refactor Haskell than it is Typescript. Both are "safe" but one is slightly safer, and much harder to work with.
And now it opens... some VSCode-esque editor in the browser that asks me to sign-in? Why would I want something even more resource-hungry and convoluted just to look up a random thing once in a while?
If you're familiar with VSCode it's quite handy. If you hate VSCode for some reason then just don't use it.
Why does ever HN thread read like a churlish blogger review of the latest installment of <popular-scifi-franchise>?
Github is great. It barely changes at all and yet it's still too much for this originalist crowd.
> In addition, it is best to use code navigation simply in a web browser
How do you define "code navigation"? It might've got a bit easier with automatic highlighting of selected symbols, but in return source code viewer got way too laggy and, for a couple of years now, it has this weird bug with misplaced cursors if code is scrolled horizontally. I actually find myself using the "raw" button more and more often, or cloning repo even for some quick ad-hoc lookups.
Edit: not to mention the blame view that actively fights with browser's built in search functionality.
Hint: Type the '.' key on any code page or PR.
jappgar commented on Trillions spent and big software projects are still failing spectrum.ieee.org/it-mana... · Posted by u/pseudolus
jappgar commented on Trillions spent and big software projects are still failing spectrum.ieee.org/it-mana... · Posted by u/pseudolus
> Gradual growth inevitably results in loads of technical debt.
Why is this stated as though it's some de facto software law? The argument is not whether it's possible to waterfall a massive software system. It clearly is possible, but the failure ratios have historically been sufficiently uncomfortable to give rise to entirely different (and evidently more successful) project development philosophies, especially when promoters were more sensitive to the massive sums involved (which in my opinion also helps explains why so many wasteful government examples). The lean startup did not appear in a vacuum. Do things that don't scale did not become a motto in these parts without reason. In case some are still confused about the historical purpose of these benign sounding advices, no, they weren't originally addressed at entrepreneurs aiming to run "lifestyle" businesses.
It is a law. The law of entropy.
Try as you might, you cannot fight entropy eternally, as mistakes in this fight will accumulate and overpower you. It's the natural process of aging we see in every lifeform.
The way life continues on despite this law is through reproduction. If you bud off independent organisms, an ecosystem can gain "eternal" life.
The cost is that you must devote much of your energy to effective reproduction.
In software, this means embracing rewrites. The people who push against rewrites and claim they're not necessary are just as delusional as those who think they can live forever.
jappgar commented on We should all be using dependency cooldowns blog.yossarian.net/2025/1... · Posted by u/todsacerdoti
If we all did it, it wouldn't work.
jappgar commented on Building more with GPT-5.1-Codex-Max openai.com/index/gpt-5-1-... · Posted by u/hansonw
Sure, but its an instruction that applies and the model will consider fairly relevant in every single token. As an extremely example imagine instructing the llm to not use the letter E or to output only in French. Not as extreme but it probably does affect.
Not only that, but the whimsical nature of the instruction will lead to a more whimsical conversation.
The chat is a simulation, and if you act silly, the model will simulate an appropriate response.
What AI does is remove a bunch of the humiliating, boring parts of being junior: hunting for the right API by cargo-culting Stack Overflow, grinding through boilerplate, getting stuck for hours on a missing import. If a half-decent model can collapse that search space for them, you get to spend more of their ramp time on “here’s how our system actually fits together” instead of “here’s how for-loops work in our house style”.
If you take that setup and then decide “cool, now we don’t need juniors at all”, you’re basically saying you want a company with no memory and no farm system – just an ever-shrinking ring of seniors arguing about strategy while no one actually grows into them.
Always love to include a good AI x work thread in my https://hackernewsai.com/ newsletter.
One problem there is that people would rather believe the AI is "dumb" than face the facts.