Type theories with modalities are currently enjoying a large amount of interest in the field of Homotopy Type Theory. I will talk generally about why this is the case and specifically about crisp type theory, a modal type theory used to investigate constructive models of homotopy type theory.