Re:Are unsound type systems wrong?
by Izkata on Sunday April 08, 2018 @03:51PM
(#16787964)
> Similarly, in formal logic "true" and "provable" are not equivalent.
This tells me you've totally misunderstood my comment. More simply, "true" and "true" are equivalent, and "provable" and "provable" are equivalent. But while "valid" and "valid" are equivalent in the other definition, "typed" and "typechecked" are not.
This tells me you've totally misunderstood my comment. More simply, "true" and "true" are equivalent, and "provable" and "provable" are equivalent. But while "valid" and "valid" are equivalent in the other definition, "typed" and "typechecked" are not.