addaon 6 days ago

I've just taken a quick glance at this, and will explore further -- but at first, it seems like it's really a good application of ad-hoc proofs to assembly code; which is a subset of what I'm interested in, but for me the more interesting thing about the paper was the structured safety proofs for things like memory safety, no read-before-write, no overflow, etc., and thinking about how this can be expanded and generalized. While for something like a bignum library (or a heap) the actual conformance to the behavioral contract will be somewhat ad-hoc, having a lot of safety contracts also proved along the way "for free" (or at slightly reduced cost, anyway) is what really draws my attention. I can see spending 2x the time writing the code, and 10x the time proving things about it, in exchange for not having to spend the 100x (DAL B) or 1000x (DAL A) time testing it.

Reply View 2 replies
  • ecesena 5 days ago

    Yeah, I hear you. Many things are simplified in this crypto code, for example there’s no dynamic allocation. At the same time it’s incredibly difficult to get a realistic model of the hardware instructions because they all have side effects. And it gets incredibly more difficult if you try to prove real world, hand optimized code (vs academic proof of concept code).

    With all this said, I think this could be a good inspiration and look forward to seeing advancements!

    Reply View 1 reply
    • addaon 4 days ago

      > Many things are simplified in this crypto code, for example there’s no dynamic allocation.

      That's okay, I haven't worked on code bases with dynamic allocation professionally in years, and even my hobby projects usually avoid it.

      Reply View 0 replies