[andyferris]

A reliable system will need a relatively formal “proof” that what it does is correct.

Code is currently the easiest and most convenient encoding for lots of folks to express such logic. So they’ll need to learn to read the syntax even if they write less of it.

So I think people will be able to put together lots of code with AI and not much programming experience, but there will be a need to ensure that it does the right thing. Now eventually the AI will create fewer bugs, infer intent better, automatically write tests, etc but even then someone needs to eg check the testset is correct.

[gpm]

> A reliable system will need a relatively formal “proof” that what it does is correct.

One of my pet theories is that this is what programming evolves to in a few decades. Programmers write formal specifications for what should happen in some very high level language. AI + Compilers + ... take that specification, implement it, and prove that the implementation is correct and performant.

Think "SQL but not just for databases".

[Tanjreeve]

So back to waiting for "the sufficiently advanced compiler"

[hnfong]

I really want to say you're right, but I'm afraid it's not necessarily true.

Before we had computers and machines, humans did all the work.

And you can't really reliably "code" humans. They misunderstand instructions. They disobey rules and regulations. They make mistakes.

But society still strived with these unreliable humans that have no "proof" whatsoever that they'll do the job properly.

In fact, these days we still often trust humans more than code, at least in areas where the stakes are high. For example, we trust human surgeons over programs that perform surgery. We trust humans to run the government rather than programs.

It's entirely plausible that future generations growing up with AI don't see the point of requiring "proof" of correctness when deploying automation. If an AI model does the job correctly for 99.99% the cases, isn't that sufficient "proof"? That's better than a human for sure.

Yeah that sounds dystopian but I don't see why it can't happen.

[andyferris]

Interesting.

I think we’ll always have code that will need to be “formal” and deterministic. Banks, voting machines, cryptography, pacemakers, rockets, etc may all need the kind of “precise” software we have today. Precise software for precise machines.

I’m now wondering if there may be a new category of programs, that are more wishy-washy yet useful in the kind of way an LLM can be today. Computer games aren’t really mission critical, for example, and I imagine we’ll see deep learning models and LLMs embedded one day. I could imagine a kid generating game logic, maps, content, etc through a more intuitive and less formal interface. I already get ChatGPT to help me cook dinner or any other number of less precise tasks. Who knows what other new kinds of automation may be this way - to produce something “good enough” like a person would.