agentultra

You have to be able to write the software yourself in order to judge the results and get good software out. Otherwise the system claims the goals are met, the tests pass, and the human driving the system puts up a new PR. If they don’t know any better it must seem like the AI system is better than them and knows what it’s doing.

All the loops and agents don’t protect you from generating garbage.

Which sucks because then how are you supposed to improve your skills when you’re just getting the answers all day… answers you can’t verify?

People are more confident than they ought to be. Always have been. But AI throws gas on that fire.

Tania Aelbi wrote a good one of her trip.

I’m working towards a solo circumnavigation myself. Love reading about the stories of others.

Or anyone else!

This isn’t for the protection of kids. It’s for the protection of profits by surveillance capitalism.

I think the controversial part is that an engineer cannot talk to or understand customers.

A test doesn’t prove much.

Highly experienced programmers seem to have a hard time understanding this.

Why do we have tens of thousands of test cases and we still find new errors constantly? Why is our software so bloated and slow? We do we still have security breaches?

LLMs can be useful tools when guided by experts. I don’t think a PM with a dream is going to cut it in the long run.

Apparently it is. Modern companies seem to prefer dysfunction over anything else. I have been trying to understand why for my whole career.

I don’t disagree. I’ve worked on teams that definitely valued the non-coding skills more and it showed in their inability to deliver on certain requirements… mainly performance and stability.

But these are skills that can be taught to individuals.

But teaching an organization that their real bottleneck isn’t how fast they’re writing code; it’s producing production-ready software that people understand and are willing to take responsibility for… that’s much harder.

Many businesses want to treat software development like an assembly line and revert back to Taylorism. It’s knowledge work and there’s no royal road. Good teams get fast when they have the right mix of skills and trust from the organization.

What we’ve been delving into for the last decade has been a decline in the value of labour and work.

“Code isn’t the hard part,” isn’t meant as an insult at individual programmers or to devalue their work. That’s being done by big tech and their AI hype machine.

The author might be missing the intent of the observation. Maybe they’re misinterpreting it.

What I, and many people who’ve said, “code was never the hard part,” aren’t referring to the skill of an individual. It’s not the hard part of the engineering process of developing software. Programming languages have manuals. Many data structures are well documented. There are frameworks for damn near everything. While the difficulty of producing code varies by the skill of the programmer and the complexity of the problem domain; writing and understanding the code is a tractable and straight-forward problem. I can and have taught many people. People can learn.

What most people are referring to is that the hardest parts of producing software are all the things an organization has to do in the production of it. It’s not writing the code that is the hardest part for an organization. It’s getting everyone to understand the problems, working together, gathering requirements, developing specifications, validating releases, testing, etc. It can often look like herding cats and is probably harder.

I think people are one factor. Source does, when done well, communicate intent and implementation precisely to other people. If the language has enough semantic information it can communicate some part of the specification as well. Knowing what to write and ensuring your software does what you think it does is an important part of a project. It takes working with people to build the correct understanding of the specification and requirements.

But to a degree it is also about the code. Sometimes your requirements are: be fast enough. In which case you need to think about code: instructions and data.

The market logic isn’t going to be defensible. The market is highly irrational and prone to be influenced by those with the most capital, not the, “invisible hand.” Cars are freaking everywhere not because they are the best solution of transportation but because people with vested interest in the sale of oil and cars made it so by buying politicians, starting political and marketing campaigns, and on for generations. It took decades for the car to become the de-facto mode of transportation in North America let alone the rest of the world. It’s not good for us. It’s highly irrational to prefer cars when freaking wildfires and climate change threaten our very existence. In a similar vein, LLMs as they are, are not around because they are necessary and superior.

> I do not miss the wall, and I will not pretend to.

The wall is the point, if you want to truly know the truth of something. I still believe there is no royal road. Taste isn’t the answer to why you would choose a bump allocator over a slab when designing a system. It is experience, wisdom, and the long hard road of trying yourself and failing. Taste comes after.

There is much joy in suffering when the result is knowing.

Too many people have tried to declare victory over software engineering prematurely and it shows.

Simulating Elevators in TLA+ is a fun exercise.

https://github.com/tlaplus/Examples/blob/master/specificatio...

Another interesting, and underrated one: hotel keys.

This brings me back. I got to work at a movie store for a while. Great times. Almost like Empire Records.

I believe there’s a small minority of LLM users who will show up to any comment thread and scream bloody murder if you post any kind of policy limiting LLM use. They seem to feel like it’s a personal attack and must justify their use of LLMs… for absolutely no reason. It’s wild.

That would be an example of, “overfitting.” It is something the AI labs are concerned about. They tweak parameters to try and avoid it.

It’s a hard balancing act to do. Give in too much randomness and you get non-sensical outputs that are difficult to align. Fit too closely to the training data and the model regurgitates the training data.

And oh, what’s that copyrighted material we never made any agreement to use doing in there?

Okay so in the sense of Lean’s kernel, we can trust it as long as we understand it. Verifying it cannot be automated therefore, according to the criterion, it must be small so that it can be verified by a human.

Does it not also follow that we should also understand the geometric kernel using a similar criterion or, what I’m trying to understand, is there a mechanism in play in this project that verifies it for us automatically so that we only need to understand the specification and can trust the generated parts?

There are some pointers to answer this question myself that I’m looking into. Neat stuff.

Right, I’m thinking of the de Bruijin criterion applied to the generated kernel in this case. That generated kernel sounds large, and being generated, I’m curious as to why or how we don’t have to verify/understand it?

What I’m wondering about is why we don’t need to understand/verify the generated kernel and only the spec?

Is there an implicit trust we must put in that kernel?

> A human reviewer only needs to read 93 lines of formal specification and run the Lean checker to certify the correctness of the kernel, skipping the intricate 1000+ lines of AI-written implementation. To prove correctness, AI autonomously wrote over 60,000 lines of Lean proofs, which also never have to be inspected by a human.

I am curious about the approach as I find claims like this hard to believe. There is a theory behind proof kernels that they must be small because they have to be trusted and verifiable by a human. Otherwise the whole system breaks.

How does one trust an LLM generated kernel is proving the right things?

Building a MUD engine is quite an endeavour in itself. Let alone the game! A good way to test your skills in networking, parsing, databases, and data structures.

I’ve been chipping away at one on my stream using Haskell. Experimenting with Lua integration, parsing, networking, STM and concurrency… currently hacking on Entity Component Systems and unboxed vectors and all kinds of stuff.

Thing is you can start small. Start with a chat server. Add character registration. Add a mob. Add some commands to interact with the mob. Just keep adding things on.

There’s a community for mud coders too. There are dozens of us.

https://mudcoders.com/

It’s a big tent and anyone is welcome in. I learned to code on my own thanks to the efforts of people to write manuals, articles, text files on BBSs and NNTP. That’s just one way.

But try the other shoe on and walk a mile. You like writing code and solving problems yourself. Everyone in the world is telling you you’re irrelevant and should start using the machine or get left behind. The future is here and you’re not a part of it unless you give up and join us. Constantly.

It was hard before LLMs to convince software developers, let alone managers and product people and everyone else, to take quality seriously. Now it’s orders of magnitude harder. Because anything you say is met with someone who doesn’t care and thinks it’s all irrelevant. The machine will get better. It will solve all of these problems. Give up.

Fortunately that hasn’t deterred craftspeople in other trades who made knives, custom cabinetry, boats, houses and the like. Sure automation and progress has made a lot of knives available. Maybe more than we need. And most of them are disposable crap. But there are still knife makers.

All this talk of being reasonable is hard to take seriously when neither side will consider the other.

It’s also possible that even after considering all of the technical features and capabilities that LLMs bring to software development that some folks don’t find the cost of using them to be worth it. So they can say, “Sure, I will use such tools when and if I deem it appropriate.” Which may be never.

But we’re in a world right now where you can be coerced into feeling like there’s no choice but to accept those trade offs and just use the LLM.

I think it’s interesting and good that there exist places for people who share similar goals. There are few places for people who want to just do programming to chill out and not be surrounded by LLM generated code.

Also the scraping situation is totally getting out of hand. Having to keep up services is not easy or fun work. It’s just toil created at the expense of many for the benefit of few.

Their adoption results are going to be biased by the fact that Google has a vested interest in accelerating adoption and have been sticking their AI products in front of everything they can. Seems like this isn’t going to be a useful data set for making policy decisions.

You should check out Borges’, The Library of Babel.

Basically if you have an infinite string of characters in some language then you have every possible book, tweet, script, scribble, and scrap of everything ever written. You just have to find it.

Thats already a large universe to cover. Programs? Much bigger set.

This seems to be grasping for analogies to make sense of the work this person was doing.

A compiler does a lot more than source code translation.

There are specifications that tell us the de jure specifications of the language, if there is one, and then we have to recognize the de facto implementations of said language. The often disagree and leave much on the table. Some times on purpose, such as implementation details, and other times by omission.

Users of this compiler expect a deterministic compilation of the source text into the target code but it’s rarely 1:1. There are optimization passes, inlining, barriers, etc.

And then there are the run-time effects of executing a program!

I think the analogy gets a little weak because natural language is not a precise enough language to specify discrete systems.

What it sounds like the author is doing is bypassing decision points with other people and delaying making decisions themselves until the LLM agent forces them to? Which is a fine approach but I don’t think the analogy with a compiler is necessary.

People seem to have a hard enough time understanding branch prediction and thread barriers.

That will depend on your life goals.

There are cabinet makers who still make pieces by hand with hand tools. They charge whatever they want and do well. Not everything is Ikea.

It's not hard to observe what the tools and systems can do. It's impressive. But I suspect for some the trade-off is not worth it based on their principles. No amount of disbelief or encouragement will change that.

You still need an expert human to drive an LLM. And even then, with C, you need to be very careful. LLM’s generate lots of code. Code that has no obvious errors in it. The kind humans aren’t good at picking up on their own. You need other tooling in place to support human experts to prevent this kind of stuff as you would in a non-LLM contribution.

I always have to ask people, correct with respect to what?

The reason being that most software developers aren’t very good at specifying systems precisely enough that they can confidently determine whether their program does what they think it does.

We don’t need to specify systems to the rigour of mathematical proofs every time, of course. The point is that spoken language isn’t precise enough to measure correctness against.

When you suggest that the difference in correctness is huge, I can’t really understand what you mean. Correct with respect to how you think good software should be written? Correct with respect to informal specifications written in prose? How?

I know that the frontier models have large contexts and can compress a lot more tokens from their training sets. But how does that make it able to read your mind and make formal what is ambiguous or informal?

Wild idea: just write code.

I know. It’s an unbelievable concept in this AI era. Write code? Isn’t that what dinosaurs did?

If you expect that a human will need to read and maintain that code you might as well write it for them. You’ll get annoyed by having to read overly-verbose copy-pasted code. So will they. So write the code yourself and bringo: you’ll fix things yourself and write things in a way that makes sense for other humans to maintain.

Or you can come up with a convoluted web of markdown files to try and coax your agents and loops to understand what future human maintainers will expect the code to look like.

I’m not sure what path will be easier in the long run. Anyone inherit a loop-based agent-driven code base yet and have to try to understand it?