When I look into the details, all it says is that a successful type-check of a program gives a proof of the existence of a program of that type.

If course this isn't quite true. Other interesting things which are said include the idea that a proof of a conjunction can be handled as a pair of proofs (one for each element of the conjunction), and a proof for a disjunction can be a proof for either side, and so on; so in a sufficiently rich type system, we can leverage the type machinery to do logic, using product types as conjunctions, sum types as disjunctions, and so on. A proposition is then modeled as a type for a proof. An implication is a function type, proven by a procedure which transforms a proof of one thing into a proof for another.

Still, I can't swallow "programs are proofs / propositions are types".