You don't. You place unwavering faith in the machine god.
This is why, for formal methods to really be the next step, we'll need deterministic source to CoC language compilers, and we'll need to go back again.
Lean is kind of an unfortunate, cargo cult choice because it only compiles to C. Really for software we should use a prover that has a lot more targets, like Danfy. Even Rocq (formerly Coq) can compile down to several functional languages, which is more than we can say for lean.
As usual, the AI crowd latched on to the first solution that came to mind, and thanks to its prominence in mathematics applications recently just lazily are starting to try and apply it to computing, without actually understanding anything or weighing trade offs. Of course, now we are basically stuck with Lean since the models will have been trained hard on it. At least it's a CoC language, but now we need to build a bunch of extra compilation around it for this to really work.
Most of this feels fairly orthogonal to the question asked. And the reasons lean are chosen are fairly simple: it is designed to also be used for programming and it's actually successful. Compiling to C is fairly obviously a bad choice (well I guess not obviously, people keep implementing languages this way for some reason) but arguably one of the least important factors in choosing which prover to use. The alternatives to lean would be Idris (which is both unsound and unpopular), ats (which is unpopular) or rocq (which is more reasonable but still is mostly an academic project).
Compiling to C seems obviously an excellent choice for compiling a language to. It is a good choice as a target language, and one can rely on a lot of existing tooling, a stable standard, good interoperability, and wide platform support. It is also simply enough to be modeled precisely.
You'll love Correction if you have a taste for experimental literature. I've have all of Bernhard's novels. They are (mostly) uninterrupted walls of text. They can also be quite depressing. You'll likely either love them or hate them. Correction is probably the most exemplary instance of his style and experimentation, and maybe his best novel, but Concrete and Extinction fall into this category as well. Wittgenstein's Nephew, Frost, and Woodcutters are more approachable if you want to ease into it. Starting with Correction might be a bit off-putting and intense depending on how often you read more experimental/stylistic literature.
The key is the information environment and its reshaping, as you noted.
Every technology, even technologies that are, from the limited and naive perspective of the user, "free" (LLms can do what I used to do a lot faster than I can, and I don't need to maintain them right?) is not actually free. All technologies bring about their own demands and need for maintenance. Often they don't actually eliminate labor, they just shift it to new areas.
Consider LLMs. Even at the user level they have created their own information ecosystem and new grunt work and overhead. Now you have to prompt, you need to organize and manage context, skills, memory. You need to keep up with model releases. You need to be more vigilant reviewing things, the list goes on.
At a higher level they create even more toil, we need to maintain vast electrical supports and data infrastructure, data needs to be amassed continually for training, the information environment needs to be filtered and sorted more than ever as it gets flooded with slop.
This is the grand irony of technology. It's actually pretty rare for it to just be a total labor saving device. More often its real benefit is rearrangement of the world's structure and resources to move labor to more optimal places for certain needs (for example water supply systems).
This rearrangement also often rearranged financial resources and power. The big problem with LLMs today is that this aspect of the rearrangement is one of great concentration, and it's concerning (employers having a lot more power to extract labor from employees is one example)
Completely agree, it doesn't help that the models all seem to promote this behavior by writing everything from scratch most of the time.
I explicitly start most programming projects with a request for existing libraries and explicit instructions to the model to prefer using them and keep our logic exclusively to what we need beyond that.
People are forgetting and/or don't realize that just because the actual generation is zero cost does not mean the code is zero cost. Every line of bespoke code is a liability. Every piece of duplicative software you produce for no reason other than "this one is mine" is polluting the ecosystem and creating a noisy landscape in which such problems will just get worse. We are seeing the complete erosion of collective contribution models which has negative implications for the collective maintenance and enhancement of shared knowledge over time.
Again, you keep using examples that are decidedly not like the examples under discussion: artistic material (actually, the article scenario is even further constrained in that it's supposed to be footage of real physical stuff not some fabricated nonsense, so yeah, no duh using generated content is a no go).
The difference between real and artificial is called error, things like a generative adversarial network is developed for for the exact purpose of reducing error. Eventually you'll get a generator that mimics reality.
That's an ahistorical oversimplification that acts as if time and provenance are not a thing.
We operate within history whether you like it or not. This problematizes any abstraction that is conceived in terms of ahistorical static information and difference.
If I stimulate your neurons with a couple of electrical charges you will experience a "real" phenomenon which isn't real by any classical sense of the definition because the origins of that phenomenon are not "natural".
Well, I think a key part of it is what exactly you mean by:
> I recently had ChatGPT Astra write a bunch of short stories for me in a universe I'm fond of.
Because that way of stating it makes it pretty clear you yourself don't really see yourself as the author of the stories.
Simultaneously, you presented them to your friends as if you were the author. So basically your friends found out you BS'd them. Why wouldn't they be upset? Seems like a totally natural reaction.
Now, if you performed extensive labor to get the story into the shape it it's in, hours long conversations with the model, some manual tweaks, etc etc, maybe you have a better claim to authorship than you would if you used a one shot prompt (though your own framing makes it sound like you did very little)
I think your response misses pretty important distinctions between art and practical pursuits.
People get upset when other people use AI in the arts because the point is largely human expression. Technical virtuosity isn't even necessarily the most important thing in art (just look at modern art and how common the philistine refrain of "my kid could do that" is).
Art doesn't serve a utilitarian function. Using AI for it largely misses the point, and I think that's what people get upset about. It's like showing up to play tag and saying "actually I'm going to play hide and seek instead" you aren't following the established social norms of the game.
Contests, in general, always ways have restrictions around them, because they are meant to test particular human feats. I'm sure plenty of future contests will have rules against AI just as today plenty of contests arbitrarily limit technologies for the good of the competition (e.g. no doping in sports).
To respond to this situation by emphasizing the utilitarian function and value of AI is to completely miss the point.
And at the same time many of these distinctions are artificial human constructs.
The idea of these photography contests is nearly dead, if not dead. Much like the no doping in sports, once the technology gets too good, for example replicating the exact processes of your body the error rate on detection gets so high you might as well flip a coin. When making rules for any system you can always have adversaries. In contests you have two types of cheating you have to deal with. Cheaters that want to win, and cheaters that want to show you your system is broken and can't be fixed. The second type is the kind that shows you that your rules are arbitrary little abstractions in the shadows on the wall of Plato's cave.
So, I think it's important to bear in mind that the prophecy is to some degree self-fulfilling.
People in technology read science fiction. That reading in part informs and inspires the kinds of things they work on and explore. This is illustrated pretty directly with the new Tesla vehicle and various deferred dreams of flying cars—this is not an innovation influenced by practicality, it is influenced by regressive adolescent fantasy.
I think there's some degree of that in a lot of technical innovation. Yes, it's still uncanny how well Gibson tracked developments (or perhaps equally, how much his fiction has influenced the kinds of things people pursue, consciously or otherwise).
Huh? First of all, agents use software tools. They aren't likely to go away. It is still infinitely better to have deterministic programs for a lot of tasks whether the user is a human or an LLM. Sure, some tools like human centric IDEs will be deemphasized but those companies will build agent managers and harnesses instead.
Nerds also underestimate how how social people are. I can guarantee you there are whole segments of the economy that will not be fully decimated solely because they don't actually give a shit if an AI can do the job because the job is 99% clout and relationships.
Not sure why you got down voted. You are correct. It feels like here are no longer any adults in the room, just children who'd rather run around screaming about doomsday scenarios from sci-fi that have no basis in current reality than actually solve real problems, like, you know, climate, geopolitical instability, the several wars that are happening right now, the most corrupt political admin the US has ever seen, etc.
All the brains have been completely drained put of the tech sector over the past four years.
None of the AI fantasy doomers can actually show clearly how current LLMs will accomplish such catastrophe or get around the inevitable physical limits they will eventually hit. It's all myopic thinking that is only convincing if you are a very uncritical person.
And what exactly makes you confident these disasters won't happen? Are you equally confident AI doomsday won't happen? There's substantially more evidence for climate collapse being an impending doom than there is AI doom yet many people seem to have moved on to the latter
This is why, for formal methods to really be the next step, we'll need deterministic source to CoC language compilers, and we'll need to go back again.
Lean is kind of an unfortunate, cargo cult choice because it only compiles to C. Really for software we should use a prover that has a lot more targets, like Danfy. Even Rocq (formerly Coq) can compile down to several functional languages, which is more than we can say for lean.
As usual, the AI crowd latched on to the first solution that came to mind, and thanks to its prominence in mathematics applications recently just lazily are starting to try and apply it to computing, without actually understanding anything or weighing trade offs. Of course, now we are basically stuck with Lean since the models will have been trained hard on it. At least it's a CoC language, but now we need to build a bunch of extra compilation around it for this to really work.
reply