Yes, that's true for Coq extraction also. You can choose to extract to ML, Haskell or Scheme, but whichever one you pick the target language is basically treate

Yes, that's true for Coq extraction also. You can choose to extract to ML, Haskell or Scheme, but whichever one you pick the target language is basically treated as an untyped language. (Of course, it tries to avoid unsafeCoerce/Obj.magic if possible; if the program can be typed with just simple types, the extracted code should not have any unsafe coercions in it.)