Since the whole premise here is that formally verifying the properties of programs is equivalent to constructive mathematics, I think you might be asking for too much, modulo your definition of hero.