I feel like the point is still being missed, and it's very similar to the way software engineers are trying to cope. The argument you are making "Well yes now this part of math we will not need to do again, but now we can do this instead" however the issue with most people just don't want to do that....
Like who are we kidding, the type of nerds who were attracted to math and software were into it because we saw it as an art-form, it was a craft, it was being the only one in your city to be able to solve a complicated math problem, it was immortalizing yourself because you discovered a proof and added to the ever expanding human knowledge.
Imagine a leather workman who's life passion is making insanely high quality handbags, who takes joy in knowing everything he touches will last someone a lifetime and give them joy everytime they use it. And then not gradually, but almost overnight someone comes to his door and tells him we can make bags 50 times better than you at 1/tenth the price. But don't you worry, you can make more money overseeing the factory, or selling people on how good this bag is, and explaining that to them.
I mean, ok, that just is not what I wanted to do with my life. I never wanted to be a manager, I never wanted to be a salesman, I never wanted to be a writer. A craft I enjoy doing has been taken away from me, I should be allowed to mourn, I don't care that I can do something else since I never liked doing it in the first place. I enjoyed solving problems and writing code, I don't care if people say "well thats never what programming was about it was actually about becoming a manager all along" I never wanted to be a manager, I never wanted to manage, I never wanted to be a proof reader.
AI writes unarchitectes code if you don't have a system for developing and maintaining a consistent architecture over time. In human coding, a lot of architecture decisions tend to only live in human brains, communicated through ephemeral means (text chats, voice calls, etc) and are not concretely documented. Since LLMs don't really have a way to manage long running architectural decisions (memory systems can only get so far, like it won't capture architectural decisions if you never talk about architectural decisions), you have to (have your agent) capture architecture design within the repository.
I personally like using openspec for this, because it makes the model iteratively ask you architectual decisions, and then manages creating and accessing the documents as needed.
> AI writes unarchitectes code if you don't have a system for developing and maintaining a consistent architecture over time (...)
I work at a ~15y old codebase; guess that the famous "architecture" is - a glue of half-baked solutions, unfinished ideas and inconsistencies. Recently I discovered there are 6 different ways used to create audit trails in the app. The "human memory" lives until person decided to switch job or is fired. Then the next person re-invents the wheel and cycle continues.
I suggest taking an honest look at "the architecture" people are so proud of - you might realize there is not much moat there after all. But then again - I mostly write cruds - so that's probably core of the problem, lol
> The problem with AI SE is that AI writes un-architecture-ed code
Not necessarily. I use SOTA models with established stacks like .NET which allow my agent to easily follow decades of best practiced patterns (DI, EF Core, ASP.NET Core...) so you still and up with proper architecture.
In fact I can easily still manually inspect everything bc I already know how it's supposed to be written.
From my experience, the latest models still struggle to create good architecture in the sense of good system design. You mention a couple of generally helpful patterns for the structure of the code. But they don't help much to create logical units, with intuitive boundaries, good cohesion etc. - at which even the latest models constantly make awkward decisions.
I agree, but if we go one step further, what is the goal of those logical units? If the answer is, to make the code more maintainable, then the next question is, for whom? For humans, or for llms? Is it still important that the code is maintainable for humans if no humans read it anymore?
Those are not rethorical questions, I am asking them for real. What is "good quality" code in the age of AI? If there is a lot of duplication but no performance consequences, is it really a problem if only AI modify it?
It's fair questions. I think we can see that in lower complexity products, it's already not that important anymore. But I can see that for more complex cases (I'm working on a fairly complex video game for example), the maintainability is currently still important. As the latest models would otherwise still create too many inconsistencies that they can't dig themselves out of. Who knows where we are in 6 to 12 months, though!
> But they don't help much to create logical units, with intuitive boundaries, good cohesion etc.
Completely, 100% agree on these exact points. I have access to every frontier model at work. None of them write what I would call clean code. At work the teams that have gone fully vibe-coded have repos full of broken abstractions that just accumulate over time. Eventually most of the effort of the team and their AI tokens seemingly goes to fixing issues that then break other things. Any attempt at 'refactor this mess, make no mistakes' turns into a _huge_ churn of changes ("shuffling the deck chairs") without ever really fixing things.
I am a math undergrad and I tried lean. It probably is because of habit and familiarity but I still find lean proofs harder to read than NL proofs. I wonder what if the math education switch entirely to a formal language (not necessarily Lean) will be?
"Mathematics is commonly explained and recorded in symbolic and concrete forms that are easy to communicate, rather than in conceptual forms that are easy to understand once communicated. Translation in the direction conceptual -> concrete and symbolic is much easier than translation in the reverse direction, and symbolic forms often replaces the conceptual forms of understanding."
Ask a model (dsv4.1 flash works great on this) to explain the proof to you so you can get an idea of the overall concept and structure first. Formalized math tends to encode math a certain way to make it easier for Lean, which doesn't have a visual cortex, but harder for people.
As a former math major (and developer) it bugged me that lean is optimized for WRITING proofs and not for READING proofs. I'm noodling around with a language that is optimized for reading proofs:
Assuming I am a rationalist (I honestly don't like this word, it's more of a self-identifying label; if not it is just saying something really trivial. But yet these people, probably only on LW, decide to call them so, so let's use that word) and is writing to others on this forum, I would assume that they have the same mindset and peer review standard as mine, so I would not write with defensive mindset emphasized.
reply