In software engineering, programs are usually not constructed to prove anything; this claim is just the consequence of an equivalence between logic and static typing (Curry-Howard). Programming languages do not make very good logic systems in spite of the isomorphism. They are not designed to be expressive that way. The logic system exhibited by the type system is geared toward proving trivialities about the program: mainly that its run-time translation won't misuse data. Plus it supports certain devices like polymporphism and pattern matching and whatnot.
Now instead of writing a useful program, we can exploit the type system for doing logic in a separate domain, detached from the program. The proof occurs as a byproduct when we compile the program.
Somehow we encode, for instance, the "all men are mortal; Socrates is a man; therefore Socrates is mortal" argument into types and write the corresponding code. Then when the code compiles, it verifies: yes, the argument is valid. At that point, we throw the program away. What (if anything) that program does is irrelevant; its types have proven the modus ponens as it passed through the compiler, thus quod erat demonstrandum.
That is supposedly what type is all about in a very narrow, myopic branch of computer science.