Towards A Formally Verified Functional Quantum Programming Language