Revision as of 20:33, 13 November 2014 edit Jec (talk \| contribs) Extended confirmed users 1,173 edits Add features section (placeholder for now) ← Previous edit		Revision as of 20:41, 13 November 2014 edit undo Jec (talk \| contribs) Extended confirmed users 1,173 edits Slightly less stubby →Features Next edit →
Line 65: ==Features== 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. ~~(in progress)~~ Idris is a fairly mature functional programming language similar to 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 and 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. ==References==

Idris (programming language): Difference between revisions