| ▲ | mathgradthrow 2 hours ago | |
AI is, apparently, very good at producing proofs. Formal verification of program properties was out of the reach of human labor, but may not be out of reach for 10 million instances of Claude. Software security will, by my estimate, just shift to this new paradigm. | ||
| ▲ | lioeters 2 hours ago | parent | next [-] | |
My vague hunch is that in the next few years we (humans+AI) will rewrite the foundation of software to allow formal verification of all existing and newly written code, while keeping the same languages as higher-level abstraction. Similar to Fil-C as a memory-safe implemenation of C. There will be formally-verifiable implemenation of C, C++, Python, Go, and so on. Not sure what that will look like, if it's even practically possible. | ||
| ▲ | skydhash 2 hours ago | parent | prev | next [-] | |
> AI is, apparently, very good at producing proofs. Proofs of what? Defining the problem is the part that is hard, not the actual writing of the proof. | ||
| ▲ | za_creature 2 hours ago | parent | prev [-] | |
Do _you_ have 1e7 instances of Claude? Cause this new paradigm sounds to me like "we checked, it's all good bro, trust me!" | ||