Have you read about seldo.com/posts/nobody... ? Interesting times indeed!

The AI uprising was stalled by trying to reconcile python versions on the same machine, which somehow led to a removal of system python

2/2 Pair with your colleagues, prepare a plan and reach agreement, chunk into smaller PRs, and above all make your CI as truthworthy as possible (unit tests, e2e tests, etc). Finally, the review will be eased a lot.

Yes, that's the idea :). What I've built is a small proof service: an agent reads the code, picks out the pure functions, and states a property about each one as a Lean theorem. Then Lean checks it against Mathlib.

I'm sharing the same opinion. The missing piece is formal verification, and Lean with Mathlib are the perfect combo. I have made a toy project here github.com/yamafaktory/... and I find that fascinating!