Discover your dream Career
For Recruiters

Top Jane Street technologist debunks ChatGPT programming

'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.

Click here to create a profile on eFinancialCareers. Comment ANONYMOUSLY on articles and make yourself visible to recruiters hiring for top jobs in technology and finance. 

Have a confidential story, tip, or comment you’d like to share? Contact: alex.mcmurray@efinancialcareers.com in the first instance. 

Bear with us if you leave a comment at the bottom of this article: all our comments are moderated by human beings. Sometimes these humans might be asleep, or away from their desks, so it may take a while for your comment to appear. Eventually it will – unless it’s offensive or libelous (in which case it won’t.)

author-card-avatar
AUTHORAlex McMurray Editor
  • H3
    H3TechSME
    8 June 2023

    FYI - F# is a functional-first hybrid language that was originally designed 20-or-so years ago to run in .NET. So it can (when written with care) interoperate with C# - it's more popular counterpart in that ecosystem. F# also compiles to JavaScript with parallel efforts to transliterate to python, Rust and other languages. An example of F# dependent types can be found here.


    https://jackfoxy.github.io/DependentTypes/tutorial.html


    There are also dependent type examples in the Scala - part of the java ecosystem - a language that has been broadly adopted in machine learning (and "AI" more broadly) because of the popularization of the Spark framework.


    My point is that there are *plenty* of functional options in commonly used language ecosystems. Hope this helps broaden the view a bit!

  • St
    Startin
    6 June 2023

    I think you mean agda not ACTA

Sign up to Morning Coffee!

Coffee mug

The essential daily roundup of news and analysis read by everyone from senior bankers and traders to new recruits.

Boost your career

Find thousands of job opportunities by signing up to eFinancialCareers today.
Recommended Articles
Recommended Jobs
Mason Blake
Global Equity Analyst
Mason Blake
London, United Kingdom
Edgworth Partners
Private Equity Associate - Direct Lending Fund
Edgworth Partners
London, United Kingdom
Paritas Recruitment - Data & Tech
Quantitative Researcher (Systematic Fund)
Paritas Recruitment - Data & Tech
London, United Kingdom

Sign up to Morning Coffee!

Coffee mug

The essential daily roundup of news and analysis read by everyone from senior bankers and traders to new recruits.