Thread

Bend – a language that blocks AI mistakes via proof and runs on GPUs

616 points · 327 comments · nicolas-siplis

IshKebab · 1789678934 · focus · HN ↗
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.
1. gr_norm · 1789679221 · focus · HN ↗
  Is EC2 real-world enough? From June:
  <a href="https://aws.amazon.com/blogs/compute/aws-nitro-isolation-engine-formally-verifying-the-hypervisor-in-the-aws-nitro-system/" rel="nofollow">https://aws.amazon.com/blogs/compute/aws-nitro-isolation-eng...
  And for the PQ parts of Apple's crypto libraries, from May:
  <a href="https://security.apple.com/blog/formal-verification-corecrypto/" rel="nofollow">https://security.apple.com/blog/formal-verification-corecryp...
  Similar from Microsoft, from July:
  <a href="https://www.microsoft.com/en-us/research/blog/verifying-rust-cryptography-in-symcrypt-from-standards-to-code/" rel="nofollow">https://www.microsoft.com/en-us/research/blog/verifying-rust...

Unofficial Hacker News client; not affiliated with Y Combinator.