I think it's a rite of passage for every developer who ever touched the ecosystem of law to also wonder the same. Probably even since the invention of "business programming" there been developers wondering this. Many has attempting, so far, I don't think anyone succeeded.
But I'm sure someone at some point might figure it out, you never know :)
Well, there's a new batch of autoformalization attempts with LLMs now. Although I've also heard people say autoformalization will always be impossible.
It's interesting to wonder what kind of coverage Cycorp managed to achieve internally, and on what domains. Seemingly no job openings at the moment though!