Yes! Formal specs could be where the understanding of what exactly the system is supposed to do gets laid out - and ideally coupled into the verification process that the code produced actually does what it is supposed to (and nothing else...). That would be a big change!