Formal methods

You help start a new team at Jane Street that uses mathematical proof to check that software, including code written by automated agents, does what it should.

Formal methods are techniques for proving, with mathematical rigour, that a program behaves as intended, rather than only testing it on examples. The team is new and this seat is one of its first. Its aim is to make these methods as ordinary a part of writing software at the firm as type systems are today, and to use them to give feedback to programming agents and to validate the code those agents produce. A programming agent is a piece of software that writes code on a person's behalf.