Text this: Higher order logic and harware verification