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...
2. thesmtsolver2 · 1789704598 · focus · HN ↗
  Funny 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.

Unofficial Hacker News client; not affiliated with Y Combinator.