It is well-known that the types in a given programming language form a category, based on Set, with their functions as morphisms.
It is also well-known that any program is basically a proof in constructive logic - the result is called in Curry–Howard correspondence and it is used in theorem prover software like Coq and Agda.
Doesn't, then, constructive logic form a category, in its own right? The objects are logical assertions, the morphisms are implications and True and False are, as in Coq, the initial and terminal object? And if yes, why isn't that category defined anywhere?
I am asking this is because it seems weird to me that many people talk about the connection between logic and Category theory, but as far as I know no one formalizes it.