2 ms·
Funny. This is happening at work. Like, technically, we're just sysadmins with a lot of systems and different services running on those. Kinda boring, just like
by tetha 4y ago
Funny. This is happening at work. Like, technically, we're just sysadmins with a lot of systems and different services running on those. Kinda boring, just like a crud service. But if you squint a bit, we're seeing ideas of formal verification, algorithmic correctness proofs and empiric experiments creeping and seeping into gaps.
Just today, me and a coworker kinda laughed about the fact that this was the second or third time we kinda ended up with an induction proof about the overall correctness of our backup retention handling for off-boarded customers, correctness being dictated by the contractual regulations of our customers. When we stopped laughing, our team lead pointed out a logical problem in one of the steps, and we were eventually able to construct a counter-example which would violate the contracts. Dang it.
Call me silly, but at this point I'm entirely ready to take a day or three off of other work to pick up a formal verification tool to validate our backup retention strategies against the different classes of contracts we have.
In a similar vein, we're starting to work towards certifications like an ISO27001. And there is a staggering amount of similarity between policies and invariants, if you look at them on a systemic level. And from there you can enter the ideas of different algebraic constructs - just like you can have broader and narrower clasess of servers with different amounts of invariants holding or not holding for them.
On top, we've started to pull data from large numbers of system to jam them through jupyter notebooks so we can use data visualization tools to get a stronger impression of what reality is like. It's pretty interesting if you can use data visualization tools like scatter plots and such to deduce the existence of a default value for a config setting. Or, to pull data and to realize: "hello. This is reality calling. Two out of three assumptions you made about systems are incorrect."