3 ms·
> But it's inadequate for the larger problem, of whether the operation is the correct one. Huh? Types (of the sufficiently advanced kind) are one way of specif
by kmicklas 9y ago
> But it's inadequate for the larger problem, of whether the operation is the correct one.
Huh? Types (of the sufficiently advanced kind) are one way of specifying behavior in the same sense as TLA+ and other models. The difference is that type theory provides a coherent story for how to form entire systems like this in a composable manner. Traditional modeling/spec languages, not so much.