「蝉语 / Cicada Language」一个可以用来辅助数学定理之证明的程序语言

欢迎大家转发给可能会感兴趣的朋友捏～

厉害，虽然我觉得这里的没几个知道什么是 DT 的…

非常优秀！《蝉语独白》简直可以作为编程的启蒙教材，逻辑清晰得不得了，深入浅出，行文流畅且有文采，页面设计也完全符合平面设计的基本原则，牛人啊。

催更

厉害，之前在推特上看到了。
希望辅助证明的工具越多越好，不过现在看来最大的问题还是学者不大接受这类工具😂

我看了半天

「断言」的定义

但全文没有讲到「断言有什么用」，语言中也没有与断言相关的语法

好强

我又反复看了几遍那篇《蝉语独白》
然后又看了半天英文那版文档……
本来还想直接从单测里找 examples 的但源码里居然没有测试


> We can use check! <exp>: <type>, to make assertion about an expression's type.
看起来「 make assertion 」的含义跟既往理解没什么区别，就是判断一个命题是否正确
但下面的正文里写的意思好像说
「我能为<exp>:<type>下定义」（「我能定义一个<exp>:<type>为真」）
一样。
列举的所有 !check <exp>:<type>我都没看到结论，即断言为真还是假，搞得我一头雾水

--------

然后在「 built-in types 」这章里塞了 Equal ，本来还以为有什么可等性的定义方法，或者可等类型是什么特殊类型
然而似乎也不是
是说 Equal 这个三元组是一个抽象类型？
但是又有一句
> If the two elements are actually not the same, we can still use Equal to create a Type, but we can not construct elements of this type
…………我就搞不懂了如果「 Equal(X,Y,Z)三元组」这个类型是抽象的，那么去哪，谁来判定 Y 和 Z 是不是相等的？能不能 construct 它的实例到底是怎么判定的？

--------

> If Nat is the most basic datatype, List is the next basic datatype.
我猜原意是「如果说自然数算是最基础的类型，那么 List 可以说是第二基础的」
这个 if 就很没逻辑……
然后 List( 这个括号里的参数是一个类型对吧，换言之
List(T)是一个泛型，T 作为构造类型的一部分？
那这样理解的话 Equal()也是一个泛型，List 的参数列表是类型，Equal 里却可以有表达式……为什么？规范是啥……

然后这一节还似乎想讲讲 list 上的归纳法
我 ctrl+f 了一下没看到 return induction ( 这个 induction 函数是哪讲的就放弃了





我的耐心仅够支撑我研究到这，抱歉……
p.s.
话说启发点是 coq ？文档全文也没看出来如何 prove something ，甚至如何定义公理都没讲明白，更别说推导机制……

Emmm 哪位老哥用它来证明一下勾股定理让菜鸡如我理解一下？

有意思

@GeruzoniAnsasu #8

> 列举的所有 !check <exp>:<type>我都没看到结论，即断言为真还是假，搞得我一头雾水

这个 check! 的意思是要求编译器进行类型检查，即 check <exp> against <type>，如果 <exp> 确实是 <type> 的 inhabitant （或者说 <exp> 具有 <type> 类型），则检查通过。否则应该产生一个类型错误。

> 本来还以为有什么可等性的定义方法，或者可等类型是什么特殊类型。然而似乎也不是。是说 Equal 这个三元组是一个抽象类型？我就搞不懂了如果「 Equal(X,Y,Z)三元组」

「相等类型」相关的内容非常复杂，与这门语言选择的类型论有关。我太菜了，可能回答不了这个问题。

> 那这样理解的话 Equal()也是一个泛型，List 的参数列表是类型，Equal 里却可以有表达式……为什么？规范是啥……

这是 dependent type （依值类型），即类型可以依赖值。在 DT 的语言中，类型和值并没有什么不同。

> ctrl+f 了一下没看到 return induction ( 这个 induction 函数是哪讲的就放弃了

这个 induction 可以视为「模式匹配」，是编译器内建的操作（比如 rust 的 match ），是一种对归纳数据类型（比如 Nat 类型）归纳证明的一种方法。你可以理解为「分类讨论」。

> 文档全文也没看出来如何 prove something ，甚至如何定义公理都没讲明白

文档这一部分： https://readonly.link/manuals/gitlab.com/cicada-lang/cicada/-/datatype/01.1-proving-theorems-about-nat.md
以加法交换律为例展示了证明，即：add_commute(x: Nat, y: Nat,): Equal(Nat, add(x, y), add(y, x))
这个函数签名的意思是：对于任意两个自然数 x y ，都有 x + y = y + x
而这个函数的 body 就是对这个命题的证明。
关于这个问题，更多可以参考： https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence

@Ultraman 这里有对「加法交换律」的证明哦：

https://readonly.link/manuals/gitlab.com/cicada-lang/cicada/-/datatype/01.1-proving-theorems-about-nat.md

@cmdOptionKana

为这个项目努力了很久很久了，还是第一次见到这样的这样的评价。

有点感动，谢谢你。

@GeruzoniAnsasu 源码里有非常完备的测试哦。

详情请见这里的 `tests/`： https://github.com/cicada-lang/cicada/tree/master/docs

另外，其中的 `manual/` 和 `articles/` 也算是带有文档的测试，运行测试的时候会跑到的。

@GeruzoniAnsasu 感谢你的反馈！我会仔细思考你提到的点，逐步改进我的文档的。

博客有 rss 吗

@lance6716 目前还没有 rss 。
不过有 Twitter： https://twitter.com/CicadaLanguage
和 Telegram：@CicadaLanguageCN

加了一个 sponsors 页面 https://cicada-lang.org/sponsors