3 ms·

https://blog.janestreet.com/formal-methods-at-jane-street-index/ https://blog.janestreet.com/formal-methods-at-jane-street-in... I thought this article from Ja

• exogenousdata 2mo ago
  And it’s not just blogs. They’ve got an open job posting [0] for a ‘Formal Methods Engineer’. [0] - https://www.janestreet.com/join-jane-street/position/8585303002/ https://www.janestreet.com/join-jane-street/position/8585303...
• rstuart4133 2mo ago
  And this pairs nicely with Jane Street's observation that agentic coding changes the formal proof equation: https://news.ycombinator.com/item?id=49064854 https://news.ycombinator.com/item?id=49064854 Formal proofs of code are almost beyond the capabilities of the best human programmers (3.7 lines per day!), but LLMs can bash out code at an amazing pace. It's often crap, sadly, but the proof they are bashing out is the hard bit. If possible at all, the task is EXPTIME. Verifying the proof is only P, so when it's wrong you tell the LLM to do it again. A stable agentic loop is what makes it possible. The results in the article I linked to speak for themselves.