That itself may be tricky. Suppose you proof system tells that the proof is correct — how do you verify it is proof of the assertion you want, unless you have beforehand written the "test harness" by hand? At least in programming, formally checking that the code does exactly what is required is orders of magnitude harder than simply writing code that compiles.