deterministic

I judge articles by the value delivered. Not the writing style. And this article is very much high value compared with the a-simple-idea-explained-with-a-wall-of-text low value/noise most HN stuff has become.

What an excellent read. This is why I read HN. Thanks!

The moderator is basically the equivalent of the environmental evaluator in a genetic/survival of the fittest algorithm. So of course the moderator will shape the outcome. No surprise there.

Not my experience at all. Quite the opposite. At my workplace we use AI to improve code quality and software design every day, far more than we used to, because AI makes it fast and easy.

I’m not convinced code reviews add much value, unless most of your co-workers are less capable and you’re trying to improve overall quality.

That said, I get a lot of value from talking to experienced developers before writing any code.

> I've also tried to understand the code that AI writes, but it's often insane and untangling it would slow me down

I hear that a lot, but it is very different from my experience using Claude Code every day. The code it generates is pretty much what I would have written myself. My colleagues have always said my code is easy to read and understand, so hopefully it is not just because my code is insane too :)

So I wonder: how are you using LLMs?

> and so has the output quality

Not my experience at all. The quality has gone up dramatically. Because we also use LLMs to make large scale refactorings that cleans up the code and use it to find lots of bugs that would otherwise have exploded in production at some point in time.

I would cry a lot. I love my Claude Code :)

But other than that nothing really.

I can't remember what I wrote yesterday. So it forced me from an early age to not write spaghetti code. Which is a real advantage it turns out when working on large projects. And an even bigger advantage when using LLM's to code.

The platforms unfortunately have zero incentives to help you manage your addictions to the "wrong" things. Quite the opposite.

The same way bakeries and cafes have zero incentives to not be your local sugar addiction dealer.

Marx was extremely simple minded when it came to human nature. That’s the problem with all utopian ideas and all idealistic philosophers and economists: the assumption is always that humans will behave in some idealised way. While in reality greed, cruelty, corruption, treating other humans as inhuman or slaves is part of human nature. Not the only part of course, but probably the most important part when looking at the very long list of disaster we call history.

Not at all. High level objectives from above are transformed and interpreted and subdivided by lower levels into actual planning and execution.

Also, a corporation is infinitely more simple to manage than a whole country.

Non-paywall link?

You are absolutely spot on. I’ve worked on a number of game development teams, and it was always clear to me that the game was created by the whole team.

Great gameplay ideas came from programmers, artists, designers, marketing people, testers, and many others. All those ideas were then brought together into one unified product.

Please write an article about this.

The trick is to start with the smallest possible implementation of a spec and proving it correct. You then add a more advanced and faster implementation and prove that the 2nd implementation implements the 1st. Etc. etc.

It's called refinement and it's a great way to prove really complex software correct. You basically have a formally proven correct chain of software from simple to advanced. CompCert is an example of how to do this.

Completely and 100% utterly wrong. LEAN is a functional programming language with a type system strong enough to express cutting-edge mathematics and proving it correct. And yes it also has DSL's built on top of it optimised for doing math but that is an extra.

LEAN is exactly an expressive type system. Nothing more. The amazing thing is that the type system is so powerful that you can express cutting-edge mathematics with it and prove it correct.

In other words, proving something is essentially the same thing as type checking.

It absolutely blew my mind when I finally understood how it works. For that reason alone, LEAN is worth diving into. :)

I was fully prepared to hate this article, given the long list of previous “I have no clue how formal proof tools work, yet have strong opinions about how useless they are” articles.

Instead, I was pleasantly surprised by how balanced it was.

What convinced me that formally proving software correct is possible were seL4, CompCert, and my own experience proving small projects correct using Lean and Rocq.

seL4: The US military and NSA tried to break seL4. They failed.

CompCert: Researchers tested CompCert against five leading commercial and open-source C compilers. Every compiler except CompCert had bugs. Not just a few, but hundreds. CompCert had zero.

And there are now many more commercial examples of software being formally proven correct.

Maybe in the future the difference between being a programmer and being a Software Engineer will be that the software you write is proven correct.

That might actually happen with the help of AI.

> In the future AI code inevitably will embody most good software engineering practices

That is not inevitable. It's a big maybe.

Today's leading-edge AIs are still far from being good software architects. I constantly have to steer them away from producing spaghetti code.

Maybe AI will get there one day. But today's leading-edge models aren't even close yet.

My experience as well! My memory is terrible. I often can't remember what I worked on last week. But I've always done well academically and at work because I'm good at deriving solutions from a few core principles and understanding the problem at hand.

That's why computer science suits me so well. I'd probably make a terrible doctor, though, since medicine involves remembering a huge amount of information.

I’ve managed large software teams for 10+ years and also worked as an individual developer.

In my experience, most middle managers, probably 90%, have no clue how to manage software developers. It’s not that hard to manage teams IMHO, but you need to focus on the right things.

> most people don't realize how good LLMs are at 3D these days

It seems to work well generating static 3D models. However typically with way too many triangles and no skeleton unless it is a human.

That's my experience anyway. I would be happy to be proven wrong.

Amazing hackers are everywhere. Not just in the (tiny) Lisp community.

Unless you think that the inventors of C, C++, Unix, Linux etc. were not amazing hackers?

My experience: C++ is an ideal language for AI-assisted software engineering. It just works beautifully with Claude Code.

> Lisp was the original language of AI

Ahhh so that's why the AI winter happened? Wrong programming language? /s

I know a lot of amazing developers, but they never claim to be “elite” or make similar nonsense claims. They let their work speak for itself.

Game designers in the games industry use Lua (and other script languages) all the time without being programmers. That doesn't mean that those languages are more "elite" than others.

Also, I taught myself machine code programming when I was 11. Just using a book (no help, no internet). So don't underestimate what kids can learn.

It seems to happen a lot with Lisp enthusiasts for some reason, usually without any evidence to back it up.

It always makes me laugh because the real world runs on C/C++, not Lisp. So perhaps by “elite” they mean something other than being successful in the real world? Maybe they think they “get it” while everyone else doesn’t, which somehow makes them “elite”? A bit like conspiracy theorists who think they’re among the few smart enough to know the “truth.” Not sure.

> The United States has the best engineers because it pays the best

Nope. There are many counter examples of companies being world leading without paying world leading salaries to their engineers.

It's a big mistake to believe that the only thing all engineers care about is $. Yes it is true for some engineers but not for all.