1. 18

  2. 3

    This is a nice overview of what is feasible today: careful coding with strongly typed languages, manual vetting of dependencies, and background work on formally verifying small critical components. Very heartening to see!

    1. 1

      yea, this is a great application of the quality spectrum. What’s interesting is, they don’t even mention unit testing. They start right at fuzzing and go all the way to formal verification.

    2. 1

      wasm has a great story for formal reasoning. Fun fact: it has a full formal specification. It also has a full mechanized proof in a proof assistant (Isabelle). If memory serves me correctly, some people were also working on formalizing it in another proof assistant.

      This makes it a very interesting choice of target for verification efforts.