A program is only correct (or incorrect) relative to its specification; if the program is correct relative to its specification, we say it implements or refines the specification. There are two ways: one, write an even higher-level specification and prove our original spec implements the higher-level spec (recursively do this as many times as you want), and two: admit the root of truth here is an idea germinated within a fallible human brain, transcribed to spec through fallible cognitive processes, with much lost in translation during transit over the fundamentally unbridgeable lacuna between mind and material world.