Agda

2022年6月11日 (六) 14:57的版本

您可以在Wikipedia上了解到此条目的英文信息 Agda Thanks, Wikipedia.

Agda programming language

逻辑与计算之间最深刻的联系是一种双关。「命题即类型（Propositions as Types）」的学说断言，形式化的结构可以按两种方式看待：可以看做逻辑中的命题，也可以看做计算中的类型。（来自《编程语言基础：Agda 语言描述》）

Agda is a proof assistant.

文学编程（Literal Programming）是用带有代码的自然语言进行编程，文学编程自由地表达逻辑，此概念由高德纳（Donald Knuth）提出，希望能用来取代结构化编程范型。

可以用 Agda 证明助理编写的规范（Specification）同时描述了编程语言以及该语言编写的程序自身。

相似项目：Idris, Coq

Agda is

@@ 第6行： / 第6行： @@
 ==简介==
 逻辑与计算之间最深刻的联系是一种双关。「命题即类型（Propositions as Types）」 的学说断言，形式化的结构可以按两种方式看待：可以看做逻辑中的命题， 也可以看做计算中的类型。（来自《编程语言基础：Agda 语言描述》）
+Agda is a proof assistant.
 [https://zh.wikipedia.org/wiki/%E6%96%87%E5%AD%A6%E7%BC%96%E7%A8%8B 文学编程]（Literal Programming）是用带有代码的自然语言进行编程，文学编程自由地表达逻辑，此概念由高德纳（Donald Knuth）提出，希望能用来取代结构化编程范型。