We have plans to implement a framework for writing high performance, GC free programs in Lean (http://leanprover.github.io/). We have spent the last year addressing shortcomings of the previous version and will be shipping a new version early next year. The new features include a high performance proof automation framework, a native compiler, a profiler, a debugger, an incremental build system, a documentation tool, an FFI, including a bunch of goodies I am probably forgetting. We will be demoing Lean this year at POPL (http://popl17.sigplan.org/track/POPL-2017-Tutorials#program), and hope to cut a release ASAP.