discussion of #formal-methods in the context of #Jane-Street, including #John-Nagle. #toread
on 02026-06-14Yaron Minsky at #Jane-Street, the guy Will has been talking to, wants to adopt #formal-methods now, though previously they haven’t because of the costs. “And those costs are really high! seL4 is a great example of this. It’s a formally verified microkernel, and a profound achievement. But, boy was it expensive to do! It took 25 person-years of effort to verify 8,700 lines of C, and each line of code required something like 23 lines of proof and a half a person-day to verify.” But now they have “agentic coding”, meaning #AI.
on 02026-06-14