agentultra

I’ve toyed around with parsing the TLA+ spec and generating property based test assertions from the invariants.

It doesn’t fully close the specification gap but if it could be made robust it might be a good tool.

Generating code directly from the high level specification is called, synthesis, and is still in research mode.

Projects like Synquid[0] have come a ways but are still far from being able to express even trivial programs.

[0] https://www.csail.mit.edu/research/synquid-synthesis-liquid-...

Yes, exactly. Playing along with anti-cooperative and anti-progressive behaviour is not on the agenda. The goal isn’t to get along with everyone.

Canada isn’t that great either. We say one thing then do the opposite of that. Google is moving in to do age verification for Canadian services.

Yeah, you can go pretty far with JS performance. I’ve been a fan. I find it’s harder to maintain than C, Zig, C++, Rust, etc. It’s really easy to break performant JS code. No types, allocations are hard to control without extreme discipline. It’s so flexible and you have to give up a lot of that to get performance out of JS.

React is a whole beast.

It would be neat to see some JS devs killing some benchmarks.

You can wait for slow programs that use a ton of excess memory, sure.

Or, you can have fast programs that use memory efficiently.

You just can’t do it in JavaScript. You can get really performant with JavaScript with careful engineering for sure… but there’s a big wall of diminishing returns even with all of the JIT compilation and tracing garbage collection.

Nothing stopping those same JS developers from learning some Zig or Rust or whatever. It might actually be easier to learn than memorizing all of JavaScript’s implicit coercion rules.

But if that’s too much to ask then stay in JS land and make sure there are JS devs to write tools for!

AI isn’t replacing people. Managers and executives have been sold a product that they believe they can use to replace people. Some of them probably still hold some enthusiasm for these products. But there seem to be some that are getting wise to the fact that they’ve been duped.

An AI system cannot replace professional people. It doesn’t replicate or do the work that they do. That’s not what it is for and it is incapable of performing these tasks.

If you are using these systems you still need to know what you want and how to specify it. You can use agents to automate much of the work but it can’t tell you that your ideas are bad, that there’s a better way to accomplish your goals; it can’t tell you what you want. And if you can’t understand what it is outputting you’re failing in your primary task as a developer: understanding the problem.

I agree with the title. I just don’t think these systems will ever be capable of replacing humans. As much as product managers and executives would love it and not have to deal with us; they’ll just be shooting themselves in the foot if they try to replace professional developers with AI harnesses and fire all the people with the institutional knowledge and skill.

I think it might be possible to write a TLA+ parser and generate QuickCheck tests from it that will exercise invariants at least.

In my experience, it depends a lot on the language and the folks you work with. I’ve gotten an eyebrow and a stern talking to for using ‘map’ in JavaScript once. Some people are die-hard about statements and keywords and imperative programming and their world view and be myopic.

“We can’t have map in our codebase, we need to be able to hire anyone off the street and have them comfortable in our codebase.”

Well… since when did we hire random people off the street?

I’m used to functional programming. For me, reduce is perfectly normal. Fewer intermediate variables. No pesky statements, just a nice expression. Great.

Buuuut… some languages think implementing tail call optimization is too hard or bad or for ivory tower academics. Or they’re dynamically typed. And then reduce does become difficult to special case and make performant. So even if you like the juice it’s probably not worth the squeeze.

It was a great time working with Haskell professionally. I didn’t have to constantly defend my style of programming! But in “everything” languages… well you do. Everyone has to agree on which subset to use. And programmers are like cats. Good luck getting them to agree on anything. Even once you agree there will always be that one challenging the decree.

Hundred percent. All about trade-offs.

Although proof techniques such as proof repair have come a long way, it’s still impractical for a lot of scenarios.

TLA+ is great for systems design and such. Quick check style tests are awesome and a very low bar to clear from unit tests.

Are they slow and brittle?

I like having both. Unit tests are a decent indicator for local development. Fast, quick to iterate on. Integration tests are slow as molasses and I can’t iterate with them when it takes 20 minutes to setup the suite and run everything. Too slow. But still useful as you say.

Djikstra seemed like he was mostly against testing. But only because he was for proofs. A unit test is a single example. The real way to demonstrate the absence of errors is to prove they aren’t there (vis a vis axioms and assumptions).

But most developers don’t have the mathematical sophistication nor the time.

It’s not that unit testing is useless. Just good to know what their limitations are and to plan your testing strategy accordingly.

I think the harnesses might get better. And the alignment and pre training. But I don’t think the LLMs will get much better… I don’t have any sources for that though. Just napkin math.

At the end of the day, even if it gets to 99.9999% reliably generate what an experienced programmer would expect… you still need to be an experienced programmer to know what to want and how to specify it.

I think the experience, institutional knowledge, and process knowledge are never going to be replaceable.

You’ll still need to learn what a cache miss is and how the heap works and when to use skip lists and all that. Otherwise you will just generate slop. An AI system is not able to replace a human.

“I built a thing with AI and I don’t understand it. I want to make changes and fix things and have no ability to theorize why it fails or how to fix it.”

Oh my. See, you have to be able to program it yourself before you can build it with an LLM. Otherwise you have no way of judging the output. AI isn’t going to make you a programmer.

Learning to program is.

Interesting article. My advice is to do it the old fashioned, hard way. There’s no royal road to knowledge, skill, and learning.

Might be because most hit their maximum growth but need to keep growing indefinitely or risk becoming a “mature” company?

I think we’re more likely to die of starvation from economic collapse, heat related stress, and complications from Long COVID than an algorithm waking up and destroying us.

Unfortunately our list of potential extinction events are far more banal than these self-aggrandizing prophesies from the oligarch class.

I’m the opposite. I don’t believe there is a royal road to understanding anything. For me, the process of programming involves frustration. That is usually when I find my greatest insights.

Syntax isn’t a big deal. Names either. You can look them up. Remember them. Language gotchas are annoying and sometimes problematic.

To me, our job is understanding problems. And for me, understanding the problem involves wrestling with the code. I learn much from modelling problems in code, building theories, testing them.

Once an LLM system has generated some code I haven’t learned anything. Even when I read through the solution. It doesn't require the same activation of my brain. There’s nothing quite like working through the problem yourself.

LLMs definitely feel like they are draining my passion for computers. There were plenty of folks who checked out or were never truly passionate about programming. Now they’re louder than ever. “Nobody cares about code,” and, “optimizing is a waste of time.” Now we don’t even want to understand how it works, or whether it works at all. They repeat the lines their master have told them: get on board or get left behind.

I’m pretty sure I am risking getting, “left behind.” But I’m okay with that. The tech is truly the least interesting thing to me. If I don’t have a career in 10 years… oh well. I’ll still be programming.

The EPA hasn’t been able to regulate anything since it’s been gutted by the current administration. Of course it’s going to scrap rules. We’re not even allowed to measure the effects of climate change.

> In practice, when you reach for a database engine you're actually reaching for four basic features: unique constraints, transactions, indices, and history tables.

That might be a very specific assumption. What about serializability? Replication? Materialized views? Procedures? Locking? Access control?

It’s cool to experiment and try new approaches. Neat one here.

Could still end up moving to Postgres.

You can work around 12. with constraint satisfaction solvers.

After generating the level structure, emplace an entrance and exit such that they are maximally apart. And emplace a strong monster in one of the rooms around the exit. And emplace a health potion in one room before the strong monster. And emplace treasure in the exit room.

That sort of stuff and be specialized and coded towards your particular games structures fairly easily.

Scale is much harder though. In something like NMS it’d be intensive doing such a constraint solver on the whole galaxy. Might work in chunks or regions though.

No. Dear lord no.

One thing I am getting really tired of is the growing inability to distinguish legitimate sources. I don’t want to have to play, “can you tell the difference?” It’s not fun being had by a liar.

I want human written content or nothing at all. I care about the struggle. I like the spelling and grammar mistakes. I enjoy the story between the lines. I like the growth of the author and watching them and their work evolve.

Generated fiction is boring because it has none of that. There is no life in it. No author.

“A human wrote it,” is a light trick. Ok, who? Where are they from? If you have to lie to give answers in order to convince someone they like the story you’re not proving that people prefer AI stories in my estimation: you’re proving that the test is a convincing lie. And maybe that people are gullible.

We already know how to solve for climate change. All that is lacking is political will. Not AI.

Why not both?

> just about everything in modern life, from streaming Netflix to running a dishwasher, consumes water at levels that can be portrayed as wasteful by hair-shirt environmentalists.

Ad-hominems in an Economist article. This reads more like an opinion piece than reporting. There are plenty of documented problems with water usage of data centres. Some can use it efficiently but it costs more to do so and many (most?) do not.

We are also in a time when most people would prefer to use that water for drinking, washing, cleaning… basically anything except data centres.

Don’t think many people are going to read this and think, “Gosh, I was a fool!”

Big congratulations to the world leaders and policy makers who were at the signing of the Paris Accord. Went home. And did very little about it. Now we output more CO2 faster than we ever have in our entire history.

At least the economy is doing okay… oh wait.

Maybe the reason action hasn’t happened is because the solutions would drive down income inequality?

Was hoping my kids wouldn’t have to live with the worst of it but it looks like we failed at that.

It is a bit of a pedantic argument but I get upset when people misuse the term, abstraction, and can feel the impulse to write a blog post like this.

I think it’s important to make clear the RL part and the alignment and parameter tweaking that gets done on models and inference engines. It makes them more understandable as mechanisms and less like wish-washy super intelligences that make their own decisions.

When these systems win math Olympiads, it’s not terribly surprising or interesting to me. Of course they will: we trained models to play nearly optimal chess games and Go. You tweak the rewards and sigmoid and you start optimizing the function towards your goal. This is how learning systems of all stripes work.

It’s still next-token predicting at the end of the day. I don’t think it’s a reduction-ad-absurdum.

But a lot of people still call it, “intelligence,” and try to use language that obscures what is happening in terms of anthropomorphic behaviour and not machine ones. That really does influence how we use these tools and profits those who would use them on us.

> If many people hated their products, they wouldn't use them

This might be true in a true, free market without monopolistic collusion and the abandonment of antitrust regulation and enforcement in the US.

In many cases people don’t switch to something else because there isn’t an alternative. Or because they don’t know how to change the defaults that come installed on their computer. Or they get a big scary warning if they figure it out and try.

I would have a hard time believing anyone who said Google was competing fairly and not juicing their numbers with Gemini. Like with search and ads, they have a lot of vested interest in profits and little regard for much else. There’s no reason to. Almost all safeguards on corporate behaviour have been taken off in the last bunch of years.

Google jumped at renaming Lake Ontario.

Of course they’re going to shove AI mode as the default on search and claim every user loves it.

I wrote an interpreter in Zig not too long ago. I’d definitely recommend more folks try it out. It’s a straight-forward enough project to dip your toes in emulation and see if it’s your jam. And it’s not a big enough project that you’ll get overwhelmed before you finish.

Not that much of a difference for the average or lower classes of people that outnumber the rich by quite a lot. It would have a great and positive impact for them.

I don’t like LSPs. They’re slow and bloated. I’ve been using clangd but I think I’ll stop. It’s slow as molasses. It constantly tries to insert headers into source files that cause compilation issues. There are easier and faster ways to jump to definitions.

I don’t use LSPs with Haskell anymore. I work on multiple projects which use different versions of GHC and the base library which means having multiple LSPs installed for each one. Trying to get eMacs to reliably detect which project is using which version is not something I have been able to figure out. Plus it’s slow and uses way too much memory.

At current job I’m doing C# and man does the ecosystem there really push you to use an IDE. Most of my org uses Rider. I find it just as fascinating that people actually like using tools like it. Too bad it doesn’t have a decent text editor built in.