A few months after reaching what could be considered alpha stage, Idris 1.0 is out, writes Idris creator Edwin Brady, Lecturer in Computer Science at the University of St Andrews, UK.
The key point in Idris, being now 1.0, is its core language along with the base libraries being considered stable, meaning that future 1.x versions of the language should guarantee backward source compatibility. Since the alpha release, Idris evolution has focused on tools and library support, while the language has gained new pragmas to enable less stable features, and a new LinearTypes language extension. Still, there is a lot of room for more contributions, says Brady, in particular to improve the compiler and runtime efficiency, as well as to fix the over 200 bugs that are currently open.
Although Brady believes that Idris is primarily a research tool and that it is currently under-stuffed to be considered production-ready, the interest in the language has been growing, as attested by the recent publication from Manning of Type-Driven Development with Idris authored by Brady himself, the rising number of contributors to the GitHub repo, and recent academical work. These could be the signs of an incipient Idris community, although it could still be too early to say. In conversation with InfoQ, Brady has remarked the following:
It's certainly nice to see a growing interest in Idris! There's still
lots of work to do, but it's good that we have a stable language to
build on now that we've reached 1.0. My immediate goals are to improve
efficiency and robustness of the core.We still have quite a few open issues, but many of these are about
tooling and usability, and many others are feature requests. If anyone
wants to get involved, the ones tagged as "Low Hanging Fruit" are good
places to start, and the Idris community will try to help if anyone has
any questions.
Idris is a purely functional programming language that aims to make type-based program verification techniques available to a larger number of programmers, while retaining its focus on being general-purpose and efficient enough to be used for system programming as well. You can start learning about Idris by reading its tutorial. Also, make sure to read about the trade-offs of programming with dependent types.