First steps towards correct system synthesis of system code