技术控

    今日:162| 主题:49347
收藏本版 (1)
最新软件应用技术尽在掌握

[其他] Towards Idris Version 1.0

[复制链接]

立即注册CoLaBug.com会员,免费获得投稿人的专业资料,享用更多功能,玩转个人品牌!

您需要 登录 才可以下载或查看,没有帐号?立即注册

x
Now that the language is getting stable, and that the Idris book,    Type-driven Development with Idrisis nearing publication, it’s getting close to time to release version 1.0.  
  We’ll shortly be releasing Idris version 0.99, which is essentially an alpha release of 1.0, and we’ll keep releasing updates until 1.0 is ready, probably around February 2017. There’s still plenty to do, which we’ll be working on over the next few weeks, mostly relating to stability and efficiency, fixing as many issues as we reasonably can, and committing to various minor decisions that we’ve been putting off.
  What do we mean by “1.0”?

  Mostly, what we mean by calling a release “1.0” is that there are large parts of the language and libraries that we now consider stable, and we promise not to change them without also changing the version number appropriately. In particular, if you have a program which compiles with Idris 1.0 and its Prelude and Base libraries, you should also expect it to compile with any version 1.x. (Assuming you aren’t relying on the behaviour of a bug, at least :))
  Specifically, when we release version 1.0, the following will be stable:
  
       
  • All of the language, except those parts which require a      %languagepragma to use   
  • Everything in      prelude, except      Language.Reflection   
  • Everything in      base, except modules in the      Language.Reflectionpart of the hierarchy  
  In version 1.0, a    %languagepragma will be required to access: reflection mechanisms (that is, error reflection, elaboration reflection and reflection functions), uniqueness types and    dslnotation.  
  The other packages distributed with Idris,    contrib,    effects, and    pruviloj, may yet change. In particular,    contribremains a place for new modules to be tested, and    effectsis likely to be deprecated in favour of a    new libraryat some point.  
  Furthermore, the IDE protocol will remain backwards compatible throughout 1.0.x releases.
  Will version 1.0 be “Production Ready”?

  Idris remains primarily a research tool, with the goals of exploring the possibilities of software development with dependent types, and particularly aiming to make theorem proving and verification techniques accessible to software developers in general. We’re not an Apple or a Google or [insert large software company here] so we can’t commit to supporting the language in the long term, or make any guarantees about the quality of the implementation. There’s certainly still plenty of things we’d like to do to make it better.
  All that said, if you’re willing to get your hands dirty, or have any resources which you think can help us, please do get in touch!
友荐云推荐




上一篇:Integrating Logz.io with PagerDuty & Using Aggregations for Alerts
下一篇:微服务化改造系列之三:配置中心
酷辣虫提示酷辣虫禁止发表任何与中华人民共和国法律有抵触的内容!所有内容由用户发布,并不代表酷辣虫的观点,酷辣虫无法对用户发布内容真实性提供任何的保证,请自行验证并承担风险与后果。如您有版权、违规等问题,请通过"联系我们"或"违规举报"告知我们处理。

shunng 发表于 5 天前
顶贴不认真,大脑有问题。
回复 支持 反对

使用道具 举报

淘旅游 发表于 5 天前
生我之前谁是我,生我之后我是谁?  
回复 支持 反对

使用道具 举报

*滑动验证:
您需要登录后才可以回帖 登录 | 立即注册

本版积分规则

我要投稿

推荐阅读

扫码访问 @iTTTTT瑞翔 的微博
回页顶回复上一篇下一篇回列表手机版
手机版/CoLaBug.com ( 粤ICP备05003221号 | 文网文[2010]257号 )|网站地图 酷辣虫

© 2001-2016 Comsenz Inc. Design: Dean. DiscuzFans.

返回顶部 返回列表