Idris (programming language): Difference between revisions

Revision as of 23:31, 6 April 2013

Revision as of 23:32, 6 April 2013

Line 24:

The language supports [[Proof assistant|interactive theorem-proving]] compareable to Coq, including tactics, while the focus remains on general-purpose programming even before theorem-proving. Other goals of Idris are "sufficient" performance, easy management of [[Side_effect_(computer_science)|side-effects]] and support for implementing [[EDSL#Usage_patterns|embedded ___domain specific languages]].

Currently, Idris compiles to [[C (programming language)|C]] and relies on a custom copying [[Garbage collection (computer_science)|garbage collector]] using [[Cheney's algorithm]]. There also existsexist [[JavaScript]] and [[Java]] backends, and a partial [[JavaScriptLLVM]] backend.

==References==