agda 语言有什么优点？

V2EX = way to explore

V2EX 是一个关于分享和探索的地方

现在注册

已注册用户请登录

• 请不要在回答技术问题时复制粘贴 AI 生成的内容

这是一个创建于 3582 天前的主题，其中的信息可能已经有所发展或是发生改变。

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

12 条回复 • 2015-03-11 03:21:34 +08:00

jamesxu

2015-03-06 12:39:42 +08:00 via iPhone

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

SmiteChow

2015-03-06 13:30:32 +08:00

听都没听过

cicku

2015-03-06 14:14:19 +08:00

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

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

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

cicku

2015-03-06 14:15:51 +08:00

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

您真厉害。

cicku

2015-03-06 14:19:00 +08:00

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

请无视我的回复。

jamesxu

2015-03-06 16:01:05 +08:00 via iPhone

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

robertlyc

2015-03-06 16:02:55 +08:00

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

alsotang

2015-03-06 17:13:47 +08:00

@cicku

@robertlyc 这个说法我也听过

yetone

2015-03-06 18:41:11 +08:00

想问楼主是哪个学校。。

msg7086

2015-03-06 18:55:30 +08:00

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

bobai

2015-03-11 03:19:40 +08:00

bobai

2015-03-11 03:21:34 +08:00

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