‹ BackHN Continuity

Thread

Book review: Is parallel programming hard, and, if so, what can you do about it?

149 points · 66 comments · ahelwer

  1. thomasahle · · focus · HN ↗
    Parallel programming is a great application for LLM correctness proofs in Lean.

    You can't unit test your way out, but if you care about the code's correctness, today there's a way.

    1. 6gvONxR4sf7o · · focus · HN ↗
      My experience has been the opposite. If lean had linear types (or separation types), it would be, but as it is, Lean's just a little bit too focused on talking about results to tidily talk about how those results are computed.
      1. winwang · · focus · HN ↗
        I don't know. For many operations, you can encode "how" by saying "under any permutation of this sequence of applications". At least, for EREW machines.
Open on Hacker News to reply ↗

Unofficial Hacker News client; not affiliated with Y Combinator.