What proof systems are you thinking about? Strong static types seem the most natural way to introduce formal verification into mainstream programming to me.
(Not the parent here.) ACL2 is a prominent example of a proof assistant without a strong static type system; its object language is a pure subset of Common Lisp. The lack of static types is one of the reasons I find proving in ACL2 to be painful, but others have done amazing stuff with it.
I don't feel there's much difference between e.g. the Coq way where types are used to bake specifications + proofs into the program and the Isabelle way where you write a program with less complex types and prove properties about the program after the fact.
General mathematical proofs? If you mean paper proofs they wouldn't be considered formal as they don't go down to the axiom level.
