It doesn't really mean much, though, if the working program (proof) corresponds to a theorem like "Given an Int, I can turn it into some other kind of Int", or

It doesn't really mean much, though, if the working program (proof) corresponds to a theorem like "Given an Int, I can turn it into some other kind of Int", or "Given some sort of String, it's possible to turn it into a Boolean", or "Given an arbitrary input, I can yield some sort of arbitrary output". Those theorems are rather pointless. That's what most programs "as proofs" are like, where the value in them is in the side effects rather than their types. Now, when dependent types become more of a thing in the industry, maybe we can argue that our programs are getting more rigorous.