'AI is coming for your job' might be the most uttered sentence of 2023. Everyone is under hypothetical threat from generative AI, and software engineering is no exception.
Tools like Copilot at Microsoft already work alongside developers, making 'citizen developers' all the more efficient. There are suggestions that we'll all soon have access to something similar, but a senior financial technologist and PhD open-source contributor disagrees.
Richard Eisenberg, a functional language designer at prop trading firm Jane Street, spoke recently on a podcast by the firm about 'The future of programming.' He discussed what makes ChatGPT powered programming work, and what gets in its way.
"This evolution of AI assisted programming is not quite the sea of change others have seen it to be" Eisenberg says. "It's a big step, but it doesn’t remove the need to communicate precisely."
The complications are inherent in the nature of programming languages. Eisenberg loosely defines them as "a mode of communication that is precise. There are precise semantics to everything said in that language." Conversely, he says that "natural language is very, very squishy."
That's not to say that AI is hopeless at converting prompts into code. Eisenberg says the assistants in use today are "surprisingly powerful and can do a stunningly good job of taking a query, understanding it and providing a piece of code." Given the innate interpretability of natural language however, "they're also strikingly fallible, they make a lot of mistakes."
So what can we do to make sure ChatGPT writes our code the way we want it written?
The secret technique that could revolutionize AI coding
Prior to joining Jane Street, Eisenberg was a significant open-source contributor to the Haskell language. His most notable addition was the implementation of dependent types. This is an innovative technique that can change the entire coding process, AI assisted or otherwise.
At its core, Eisenberg says dependent types "allow you to encode a proof of correctness into your program," setting definitive parameters to ensure "your program does what you think it does."
This could be relevant when it comes to writing prompts to generate ChatGPT code.
As an example, Eisenberg brings up a simple function of sorting a list of integers into ascending order. One dependent type you could use is to ask it to display an output in non-descending order and to specify that if the output doesn't fit this description, it won't run.
There is still some leeway there. The computer could return nothing and that's technically in non-descending order. The final dependent types that Eisenberg specifies in this example is that the program "takes in a list of ints and returns a result that is in non-descending order and is a permutation of the input list."
Used with AI, Eisenberg says this can be "your input into the large language model," a method of tightening the reigns and ensuring the code written by the machine satisfies your aims. Using these precise dependent functions in your prompt will ensure the output is within the specifications you are aiming for.
Can you not just ask ChatGPT to write the function as well? Eisenberg warns against it, or says that if you do, you should at least have a complete understanding of the functions prior to doing so. "If the human is not expert enough to read the specification and know it's right, we've lost," Eisenberg says. "Now the computer can just go off and do whatever it wants, and we have no way of knowing whether it's right or wrong."
Dependent types are not a faultless fix. They can very easily come at the expense of speed which, especially in a firm like Jane Street where the speed of code is vital, can be a huge setback.
Not all languages fully support dependent types. Eisenberg says that "Coq, ACTA Idris Lean are the ones that really have embraced it." Coq and ACTA have been around since the 80s, making this yet another example of ancient coding techniques being reborn under new technology.