As far as I understand -- please correct me if I'm wrong -- F* uses dependent types as a foundation of maths (i.e. a logic) and embeds program logic via a HTT (

As far as I understand -- please correct me if I'm wrong -- F* uses dependent types as a foundation of maths (i.e. a logic) and embeds program logic via a HTT (= Hoare Type Theory). This is a very nice division of labour between programming and verification.