[oisdk]

> F* is a programming language with proof support. Lean/Coq are theorem providers that can be used to model and generate code.

Lean is also a programming language with proof support. It is very much in the same category as F* in this regard, and not in the same category as Coq (Rocq).

[clarus]

In Rocq/Coq, you have "extraction", which is the standard way to compile programs. This is how the C compiler CompCert is executed, for example. So, all of these languages are in the same category in this respect.