‹ BackHN Continuity

Thread

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

616 points · 327 comments · nicolas-siplis

  1. prmph · · focus · HN ↗
    Aren't ALL type system proof systems?
    1. gf000 · · focus · HN ↗
      Well, yeah. Most are just unsound and not too useful (e.g. can only state propositional logic statements).

      I once wrote a pretty disgusting Java-implementation of that concept. And if you didn't use the stdlib, nulls and who knows what else and you managed to return the type only using your input parameters (that is, you had your function signature as the statement you want proven and the body was your proof of that), then your statement was "proven" to be true.

Open on Hacker News to reply ↗

Unofficial Hacker News client; not affiliated with Y Combinator.