1. 8
  1.  

  2. 2

    Man reading this reminded me of how nice ghost values are. I wonder if they have a good use in unverified code. Test hooks, maybe?

    1. 1

      I’ve used ghost code to do unit tests. But that was on code that has already been verified..

      1. 2

        But that was on code that has already been verified..

        Lets assume specs are correct. The verification tools can fail [1]. Compilers can produce incorrect code [2]. Testing verified code against the spec still makes sense. Combine formal and empirical methods for max robustness.

        [1] Just found a submission illustrating that and more.

        [2] See Section IV-D of main paper of IRONSIDES DNS, written in SPARK.

        1. 1

          Yeah, you still need functional tests and whatnot. I think we can do away with unit tests however, or maybe just keep them as a way to test that the contract makes sense

      2. 1

        Hmm, for something like C you can just (ab)use the preprocessor. #if TESTING ...

      3. 1

        I’m glad that Rust is getting the idea of rules about ownership into the mainstream, but there’s a lot of ground still to tread (and re-tread) here, before we get where we need to be.