Towards a Formally Verified Functional Quantum Programming Language