← Back to context

Comment by estebank

5 hours ago

This is in effect a state machine, and when you have a type system more complex than C's you can encode state transitions in the type system (either by having state transitions explicitly return a new return type or by using sum types). You still need to architect the system to encode the invariants in types. No language will fix all logic bugs for free. But you can leverage language features to reduce their number.

Like set an generic marker struct IsEncrypted<T> where T is yes or now and only allow its state to change when proven and then write the shutdown function to only take the yes variant?

  • Yes, that would be one way of doing it. You can model off of the Typed Builder pattern:

      struct Builder<const A: bool, const B: bool> {
        a: Option<u32>,
        b: Option<u32>,
      }
      struct Val {
        a: u32,
        b: u32,
      }
      impl<const B: bool> Builder<false, B> {
        fn set_a(self, a: u32) -> Builder<true, B> {
          Builder {
            a: Some(a),
            b: self.b,
          }
        }
      }
      impl<const A: bool> Builder<A, false> {
        fn set_b(self, b: u32) -> Builder<A, true> {
          Builder {
            a: self.a,
            b: Some(b),
          }
        }
      }
      impl Builder<true, true> {
        fn build(self) -> Val {
          Val {
            a: self.a.unwrap(),
            b: self.b.unwrap(),
          }
        }
      }
    

    This won't work for everything, but it is a pattern that I find useful to ensure that things can't happen out of order.

> You still need to architect the system to encode the invariants in types.

That's the problem though, right? If it's pointed out we all agree the "do not keep credentials alive" is a property that should hold and we can leverage whatever the environment offers to help preserve it. I fully agree modern languages have amazing support for this, but in C you can still run tests. Let's just say I don't think the language's inability to express logic of this kind held all those involved back from testing for it. I personally find "we just didn't think of it" much more likely.

That said, I am not a fan of C and recommend leveraging whatever fantastic modern tooling is available to you.