agda 语言有什么优点？

[bobai]

这学期被强制要求使用的语言，不知道是不是老师讲解不清的问题，感觉各种证明十分难写。明明一目了然的事情就是证不出来。
这一语言有没有自己的优点？要不要光学会写作业就算了，上完这学期就扔？

[jamesxu]

做研究用的，可以学完就扔的

[SmiteChow]

听都没听过

[cicku]

哥哥我谢谢你...Ada 好么？

Ada 在俄语中是 Hell 的意思，这也是为什么你觉得难的原因。

主要领域是嵌入式，国防、医疗基础设施，航空管理，铁路运输用的，目前仍被美国大型政府机构部署并应用。具体应用不便透露。

[cicku]

@jamesxu 空客，波音，目前的飞机组件管理系统全是 ada 写的，学完就扔？火箭，导弹控制系统都是 ada 写的，学完就扔？

您真厉害。

[cicku]

@jamesxu 抱歉看错了。原来是 agda，那个 haskell 衍生品

请无视我的回复。

[jamesxu]

@cicku 没事，但即便是 Ada，如果楼主不做这些行业，也是可以随便扔的。但大部分语言都有自己的优势，有时候学另外一门语言时可用作对比。

[robertlyc]

@cicku Ada是为了纪念Ada Lovelace 第一位程序员 不是因为俄语

[alsotang]

@cicku

@robertlyc 这个说法我也听过

[yetone]

想问楼主是哪个学校。。

[msg7086]

Agda的证明不难啊，基本就是逻辑推导吧……
Agda我觉得和Haskell很像的地方就是，如果你没入门，那你一定会死去活来；一旦入门，海阔天空。

[bobai]

@cicku 确实是agda。。。
http://en.wikipedia.org/wiki/Agda_%28programming_language%29
你说的ada是另一个

[bobai]

@msg7086 有没有相关书籍？我现在正在死去活来阶段