‹ BackHN Continuity

Thread

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

616 points · 327 comments · nicolas-siplis

  1. delifue · · focus · HN ↗
    I roughly check it. The array looks like tree in type defintion, where indexing is O(log n), but the real implementation seem to be real array with O(1)

    The Type thing is affine type similar to Rust ownership. The array in-place mutation relies on affinity to avoid deep copying. The Data thing is reference-counted if shared, like Rust Arc. The parallel invocation is similar to Rust's rayon::join .

    About the proof system, I am not familar with formal verification, but it's obvious that the translation from business requirement to proof target still requires coding and can contain bugs. Even if proof is fully correct, if proof target deviates to business requirement then it still have a bug

Open on Hacker News to reply ↗

Unofficial Hacker News client; not affiliated with Y Combinator.