@@ -5,13 +5,17 @@ Frequently Asked Questions
55What are the differences between Agda and Idris?
66================================================
77
8−The main difference is that Idris has been designed from the start to support
9−verified systems programming through easy interoperability with C and high
10−level language constructs to support domain specific language implementation.
11−Idris emphasises general-purpose programming, rather than theorem proving, and
12−as such includes higher level programming constructs such as type classes and
13−do notation. Idris also supports tactic based theorem proving, and has a
14−lightweight Hugs/GHCI style interface.
8+Like Idris, Agda is a functional language with dependent types, supporting
9+dependent pattern matching. Both can be used for writing programs and proofs.
10+However, Idris has been designed from the start to emphasise general purpose
11+programming rather than theorem proving. As such, it supports interoperability
12+with systems libraries and C programs, and language constructs for
13+domain specific language implementation. It also includes higher level
14+programming constructs such as type classes and do notation.
15+
16+Idris supports multiple back ends (C and JavaScript by default, with the
17+ability to add more via plugins) and has a reference run time system, written
18+in C, with a garbage collector and built-in message passing concurrency.
1519
1620Is Idris production ready?
1721==========================