3 ms·
If you have to do things with type-based checking, presumably you can make two new types that are only ever output by one routine, something like ensureNotEqual
by matthewdgreen 4y ago
If you have to do things with type-based checking, presumably you can make two new types that are only ever output by one routine, something like ensureNotEqualPoints(A, B) -> (pointNotEqualTypeOne, pointNotEqualTypeTwo), err. Then you have one incomplete addition formula that takes in the two different point types. This doesn't protect you from calling it multiple times in a way that scrambles the types and breaks the invariant.
Formal verification with typechecking sucks and is very limited.
- dan-robertson 4y agoIf you have a haskell style type system you can do such a thing and have the type system prevent you from calling things multiple times, eg: data P1 a data P2 a data PointNotEqual where | T :: P1 a -> P2 a -> PointNotEqual getP1 :: P1 a -> Point getP2 :: P2 a -> Point checkNE :: Point -> Point -> Maybe PointNotEqual (+) :: P1 a -> P2 a -> Point Here when you are given a PointNotEqual, you don’t know what the type variable is, only that it’s the same between the two points. So you (ie the compiler) cannot prove that a P1 or P2 from a different call to PointNotEqual has the same type variable, so you can’t add them. But these types also mean you need to do the check before every addition which defeats the point of the whole constant time thing, so the typechecking is still limited. And I guess you can’t do it in Go either.