For mathematics is not about proofs; it is about definitions. The essence of great mathematics is coming up with a powerful definition that results in short proofs.
Or in software terms, coming up with a powerful and elegant exposed API/top level functions that don’t require peeking into the abstraction (which would imply a “longer” “proof”, following Curry-Howard).
Or in software terms, coming up with a powerful and elegant exposed API/top level functions that don’t require peeking into the abstraction (which would imply a “longer” “proof”, following Curry-Howard).