A reflective functional language for hardware design and theorem proving