One of the reciprocal outcomes of this could be method(s) to mathematically prove the 'correctness' of a computer program... Although, perhaps this is verging

One of the reciprocal outcomes of this could be method(s) to mathematically prove the 'correctness' of a computer program... Although, perhaps this is verging on philosophy: is such a process even possible? Do current (or future) computer programs involve leaps of intuition, and abstractions that cannot be mathematically codified?