Content deleted Content added
Slightly less stubby →Features |
Wikify →Features |
||
Line 67:
Idris combines a number of features from relatively mainstream functional programming languages with features borrowed from proof assistants, in effect blurring the boundary between the two kinds of software.
Idris is a fairly mature functional programming language similar to [[Haskell (programming language)|Haskell]] (albeit mostly call-by-value), with pattern matching, a rich basic type hierarchy (including machine integers, bignums, strings, floating-point numbers etc.), type classes, a foreign-function interface and imperative features encapsulated within an input/output monad. At the same time, Idris contains a reasonable proof assistant, which supports both the interaction style of [[Coq]] (tactics) and that of [[Epigram (programming language)|Epigram]] and [[Agda (programming language)|Agda]] (interactive elaboration of proof terms).
By default, Idris compiles to native code through C, but other backends are available that support compilation to Javascript and Java.
| |||