> FAANG-style companies are unlikely to adopt formal methods or relational rigor wholesale. But for their most critical systems, they should. It’s the only way to make failures like this impossible by design, rather than just less likely.
That relational rigor imposes what one chooses to be true, it isn’t a universal truth.
The frame problem and the qualification problem apply here.
The open domain frame problem == HALT.
When you can for a problem into the relational model things are nice but not everything can be reduced to a trivial property.
That is why Codd had to as nulls etc..
You can choose to decide that the queen is rich OR pigs can fly; but a poor queen doesn’t result in flying pigs.
Choice over finite sets == finite indexes over sets == PEM
If you can restrict your problems to where the Entscheidungsproblem is solvable you can gain many benefits
It doesn’t matter if you get there through Trakhtenbrot or Rice.
Codd’s normal form is a projection, it will turn your fancy model logic into classic logic.
IMHO it is always something to look for to use as a default, but fails if it is a hard requirement.
One classic way to describe the problem is the White king and Alice.
> ‘I see nobody on the road,’ said Alice.
> ‘I only wish I had such eyes,’ the King remarked in a fretful tone. ‘To be able to see Nobody! And at that distance, too! Why, it’s as much as I can do to see real people, by this light!’
Codd added nulls to handle unknowns or missing data.
The proper use of them is a complex subject. But they are required if you care about semantic correctness and not just logical validity in many cases.
Diaconescu-Goodman-Myhill theorem[0] will show the equivalence between PEM, finite indexes, and choice
> FAANG-style companies are unlikely to adopt formal methods or relational rigor wholesale. But for their most critical systems, they should. It’s the only way to make failures like this impossible by design, rather than just less likely.
That relational rigor imposes what one chooses to be true, it isn’t a universal truth.
The frame problem and the qualification problem apply here.
The open domain frame problem == HALT.
When you can for a problem into the relational model things are nice but not everything can be reduced to a trivial property.
That is why Codd had to as nulls etc..
You can choose to decide that the queen is rich OR pigs can fly; but a poor queen doesn’t result in flying pigs.
Choice over finite sets == finite indexes over sets == PEM
If you can restrict your problems to where the Entscheidungsproblem is solvable you can gain many benefits
But it is horses for courses and sub TC.