@@ -5,13 +5,17 @@ Frequently Asked Questions
5What are the differences between Agda and Idris?
5What are the differences between Agda and Idris?
6================================================
6================================================
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.
8−The main difference is that Idris has been designed from the start to support
10+However, Idris has been designed from the start to emphasise general purpose
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
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
12−as such includes higher level programming constructs such as type classes and
14+programming constructs such as type classes and do notation.
13−do notation. Idris also supports tactic based theorem proving, and has a
15+
14−lightweight Hugs/GHCI style interface.
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.
16Is Idris production ready?
20Is Idris production ready?
17==========================
21==========================