From https://youtu.be/DRq2NgeFcO0 at the 25:22 mark:<p><pre><code> 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.</code></pre>
One correction: it was only acquired by Cisco in 2011. Great that they open-sourced it though.<p>There’s quite a lot of pre-Cisco history in this paper: <a href="https://www.cs.indiana.edu/~dyb/pubs/hocs.pdf" rel="nofollow">https://www.cs.indiana.edu/~dyb/pubs/hocs.pdf</a>