I would be interested to read the author's take on F. Since they are focused on math applications in this post, and F is very much focused on verified software on not on mathematics, it is a bit off topic. My (inexpert) understanding is that F* is based on an extensional type theory (different that CoC in this way) and can, but needn't, work with proof objects, since its refinement typing can just push constraints into the SMT database. I've found it pretty light weight and "opt-in" on the dependent types, and so it seems quite nice from a usability perspective IMO. But, as I say, I think it really would not address the author's question "how do we know it's right". On this point, I think the worlds of software verification and automated theorem proving for mathematics can be quite far apart.