Idris (programming language): Difference between revisions

Content deleted Content added
m fix title, add website name
Code generation: removed vague statement
Line 97:
 
===Code generation===
Because Idris contains a proof assistant, Idris programs can be written to pass proofs around. If treated naïvely, such proofs remain around at runtime. Idris aims to avoid this pitfall by aggressively erasing unused terms,.<ref>{{cite web|url=http://idris.readthedocs.org/en/latest/reference/erasure.html|title=Erasure By Usage Analysis — Idris 1.1.1 documentation|website=idris.readthedocs.org}}</ref> with promising{{Vague|date=May 2018}} results.<ref>{{cite web|url=http://ziman.functor.sk/erasure-bm/|title=Benchmark results|website=ziman.functor.sk}}</ref>
 
By default, Idris generates native code through [[C (programming language)|C]]. The other officially supported backend generates [[JavaScript]].