[1970-01-01]

When I interviewed at AWS, I asked this question directly to their formal methods expert. Her response was two-fold:

1. All our code changes too much, we wouldn't be able to formalize it before it needed to change.

2. We already did this where we could, you just don't see it.

I didn't get the job and remain very skeptical on both answers. I think they just didn't have enough power internally to change the move fast and break everything culture for the better.

[antonvs]

Why are you skeptical on point 1?

For anything more complex than standard static type checking[], they're almost certainly correct.

[] or, say, Haskell-level type checking. Which admittedly, AWS is not doing.