I didn't mean to imply that people should be using Coq or another proof assistant in their development workflow. More that understanding formal verification aids in thinking about typed programs.

However no type system of a Turing complete programming language can ever be truly trusted as a proof system because looping forever or other non-termination can be used to prove any proposition.

  const proveAnything = <A>(): A => proveAnything()

The above function can prove any proposition including 1 == 2, by just recursing forever.

However, take Rust's ownership system for example, it uses a type system that corresponds to a kind of logic called a sub-structural logic that denies one of the axioms of typical classical logic systems, namely, the weakening axiom, e.g. a function of the type

  fn <A>(a: A) -> (A, A) { ... }

is not possible to write in Rust, but easily writable in most other programming languages. Because of this, Rust is able to "prove" that the program is free from data races which is pretty cool if you ask me.