As things stand, the executable it generates is in Scheme.

  This is running via Chez Scheme.

  Chez Scheme is something that's been developed over
  decades at Cisco, recently open sourced.

  And I thought, ok that will be a good stop gap.
  It turns out that Chez Scheme is astonishingly fast.
  So even from source, the Chez Scheme generated version
  for the small set of benchmarks I've tried has run
  faster than the Idris 1 which goes via C.

  So I guess spending 30 years of knowing what you're
  doing is quite good if you're writing a runtime system.