Agda has a compiler that can extract Haskell or JavaScript, yes. But Agda doesn't seem to be very heavily used for this purposes - Coq on the other hand seems t

Agda has a compiler that can extract Haskell or JavaScript, yes. But Agda doesn't seem to be very heavily used for this purposes - Coq on the other hand seems to have very mature extraction capabilities for Haskell/OCaml/Scheme and has been used quite a bit for this purpose. You could also of course use Idris, which directly compiles to executables.