3 ms·
Interesting... But I don't think formal software verification is going to be the answer (is that what this is? Kind of unclear.) It's too difficult and doesn't
by IshKebab 23d ago
Interesting... But I don't think formal software verification is going to be the answer (is that what this is? Kind of unclear.)
It's too difficult and doesn't scale well to many real world programs - how do you formally verify Facebook?
We'll probably be stuck with normal testing and at least skimming code for a while.
- gr_norm 23d agoIs EC2 real-world enough? From June: https://aws.amazon.com/blogs/compute/aws-nitro-isolation-engine-formally-verifying-the-hypervisor-in-the-aws-nitro-system/ https://aws.amazon.com/blogs/compute/aws-nitro-isolation-eng... And for the PQ parts of Apple's crypto libraries, from May: https://security.apple.com/blog/formal-verification-corecrypto/ https://security.apple.com/blog/formal-verification-corecryp... Similar from Microsoft, from July: https://www.microsoft.com/en-us/research/blog/verifying-rust-cryptography-in-symcrypt-from-standards-to-code/ https://www.microsoft.com/en-us/research/blog/verifying-rust...
- thesmtsolver2 23d agoFunny you say that while OpenAI and rest of the world rely on Lean and other formal systems to power through (or sometime brute force) math problems.