An important point to clarify is the meaning of "free of bugs". Correctness only makes sense relative to a specification. Only once you have decided what property you care about (your definition of "correctness"), can you start to think about how to prove it.
For safety properties (memory safety (buffer overflows, use after free, etc.), undefined arithmetic (overflow, divide by zero, etc.), unhandled exceptions, etc.), there are popular approaches to detect or prevent them automatically, via type systems ("well-typed programs do not go wrong") or program analyses (e.g., Infer).
Functional correctness is a class of properties that relate your program to a "high-level" specification. For example you may expect that a function
int sum(int* x) does compute a sum $\sum_i x_i$, and that allows you to think about that function as the mathematical sum without worrying about how the numbers are laid out in memory. Since there is no hope for full automation for the most expressive specification languages, this is an area where proof assistants have a lot of potential (and it has been active for decades).
A most popular example is sel4, a microkernel written in C and verified in Isabelle/HOL. In the following excerpt, note again the precision of "against its specification":
seL4's implementation is formally (mathematically) proven correct (bug-free) against its specification, has been proved to enforce strong security properties, and if configured correctly its operations have proven safe upper bounds on their worst-case execution times. It was the world's first operating system with such a proof, and is still the only proven operating system featuring fine-grained capability-based security and high performance. It also has the most advanced support for mixed criticality real-time systems.
For another example, VST provides a program logic for C embedded in the Coq proof assistant. VST is particularly notable because it is formally related to a verified compiler, CompCert: there is a proof that VST's program logic is sound with respect to the same operational semantics that CompCert was proved against. Software Foundations, Volume 2 contains an introduction in Coq to Hoare logic, a core idea in the development of program logics for imperative languages, such as VST.
For a functional language such as Haskell, it is a lambda calculus at its core, similar to proof assistants based on type theory (Coq, Lean, Agda). hs-to-coq banks on that similarity, by translating functions into the proof assistant's language, so you can prove any properties expressible there.