AI might help programmers become more rigorous by lowering the cost of formal methods. Imagine an advanced language where simply writing a function contract, in some kind of Hoare logic or using a dependently-typed signature, yields provably correct code. These kinds of ideas are already worked on, and I believe are the future.
I'm not convinced about that. Writing a formal contract for a function is incredibly hard, much harder than writing the function itself. I could open any random function in my codebase and with high probability get a piece of code that is < 50 lines, yet would need pages of formal contract to be "as correct" as it is now.
By "as correct", I mean that such a function may have bugs, but the same is true for an AI-generated function derived from a formal contract, if the contract has a loophole. And in that case, a simple microscopic loophole may lead to very very weird bugs. If you want a taste of that, have a look at how some C++ compilers remove half the code because of an "undefined behaviour" loophole.
Proofreading what Copilot wrote seems like the saner option.
That is because you have not used contracts when you started developing your code. Likewise, it would be hard to enforce structured programming on assembly code that was written without this concept in mind.
Contracts can be quite easy to use, see e.g. Dafny by MS Research.
I think this is longer off than you might expect. LLMs work because the “answer” (and the prompt) is fuzzy and inexact. Proving an exact answer is a whole different and significantly more difficult problem, and it’s not clear the LLM approach will scale up to that problem.
Formal methods/dependent types are the future in the same way fusion is, it seems to be perpetually another decade away.
In practice, our industry seems to have reached a sort of limit in how much type system complexity we can actually absorb. If you look at the big new languages that came along in the last 10-15 years (Kotlin, Swift, Go, Rust, TypeScript) then they all have type systems of pretty similar levels of power, with the possible exception of the latter two which have ordinary type systems with some "gimmicks". I don't mean that in a bad way, I mean they have type system features to solve very specific problems beyond generalizable correctness. In the case of Rust it's ownership handling for manual memory management, and for TypeScript it's how to statically express all the things you can do with a pre-existing dynamic type system. None have attempted to integrate generalized academic type theory research like contracts/formal methods/dependent types.
I think this is for a mix of performance and usability reasons that aren't really tractable to solve right now, not even with AI.
> If you look at the big new languages that came along in the last 10-15 years (Kotlin, Swift, Go, Rust, TypeScript) then they all have type systems of pretty similar levels of power, with the possible exception of the latter two which have ordinary type systems with some "gimmicks".
Those are very different type systems:
- Kotlin has a Java-style system with nominal types and subtyping via inheritance
- TypeScript is structurally typed, but otherwise an enormous grab-bag of heuristics with no unifying system to speak of
- Rust is a heavily extended variant of Hindley-Milner with affine types (which is as "academic type theory" as it gets)
Yes, I didn't say they're the same, only that they are of similar levels of power. Write the same program in all three and there won't be a big gap in level of bugginess.
Sometimes Rustaceans like to claim otherwise, but most of the work in Rust's type system goes into taming manual memory management which is solved with a different typing approach in the other two, so unless you need one of those languages for some specific reason then the level of bugs you can catch automatically is going to be in the same ballpark.
> Write the same program in all three and there won't be a big gap in level of bugginess.
I write Typescript at work, and this has not been my experience at all: it's at least an order of magnitude less reliable than even bare ML, let alone any modern Hindley-Milner based language. It's flagrantly, deliberately unsound, and this causes problems on a weekly basis.
Thanks, I've only done a bit of TypeScript so it's interesting to hear that experience. Is the issue interop with JavaScript or a problem even with pure TS codebases?
So is the off the cuff, stream of consciousness chatter humans use to talk. We still manage to write good scientific papers (sometimes...), not because we think extra hard and then write a good scientific treatment in one go without edits, research or revisions. Instead we we have a whole text structure, revision process, standardised techniques of analysis, searchable research data collections, critique and correction by colleagues, searchable previous findings all "hyperlinked" together by references, and social structures like peer review. That process turns out high-quality, high-information work product at the end, without a significant cognitive adjustment to the humans doing the work aside from just learning the new information required.
I think if we put resources and engineering time into trying to build a "research lab" or "working scientist tool access and support network" with every intelligent actor involved emulated with LLMs, we could probably get much, much more rigorous results out the other end of that process. Approaches like this exist in a sort of embryonic form with LLM strategies like expert debate.
I think the beauty of our craft on a theoretical level is that it very quickly outgrows all of our mathematics and what can be stated based on that (e.g. see the busy beaver problem).
It is honestly, humbling and empowering at the same time. Even a hyper-intelligent AI will be unable to reason about any arbitrary code. Especially that current AI - while impressive at many things - is a far cry from being anywhere near good at logical thinking.
I think the opposite! The problem is that almost everything in the universe can be cast as computing, and so we end up with very little differentiating semantic when thinking about what can and can't be done. Busy beavers is one of a relatively small number of problems that I am familiar with (probably there is a provably infinite set of them, but I haven't navigated it) which are uncomputable, and it doesn't seem at all relevant to nature.
And yet we have free will (ok, within bounds, I cannot fly to the moon etc, but maybe my path integral allows it), we see processes like the expansion of the universe that we cannot account for and infer them like quantum gravity as well.
