In your example, any attempt to extend the core library is fraught with error. There is no way to safely do so and transitively trust the authorship. For example:
This is legal C! The ConstantTimeInt structure does not allow the composition of operations to produce safe operations from their composition!
This is illegal Haskell:
square :: ConstantTime Int
-> ConstantTime Int
square = do
randomRIO (0,100) >>= threadDelay
return $ multiply value value
In Haskell, tight, small libraries can be written using impure constructs (as these ConstantTime things likely would be) and verified logically. Then, using the type system, that kernel can be used to create an amazing variety of strongly typed systems safely from a compact representation.
In your envisioning of a C ConstantTime library, you would never finish writing the library. If someone wanted to perform date arithmetic, you would have to implement that in your library and check it by hand and monitor it and maintain it. You could never let your guard down on any commit that would touch an ever-expanding body of code that would have to be rigorously checked to handle increasingly complex scenarios.
For example, to implement a constant time big (but fixed size) integer multiplication operation, you would not be able to trust that some other author's composition of your functions is safe purely by its type.
This is illegal Haskell:
In Haskell, tight, small libraries can be written using impure constructs (as these ConstantTime things likely would be) and verified logically. Then, using the type system, that kernel can be used to create an amazing variety of strongly typed systems safely from a compact representation.In your envisioning of a C ConstantTime library, you would never finish writing the library. If someone wanted to perform date arithmetic, you would have to implement that in your library and check it by hand and monitor it and maintain it. You could never let your guard down on any commit that would touch an ever-expanding body of code that would have to be rigorously checked to handle increasingly complex scenarios.
For example, to implement a constant time big (but fixed size) integer multiplication operation, you would not be able to trust that some other author's composition of your functions is safe purely by its type.