https://learnku.com/

Laravel 还是很火

潮流是个大摆锤，今天锤锤这，明天锤锤那。

静态型没啥未来。研究研究 SICP，抽象才是编程技术绝妙的地方。

比如你在书写数学，不会关心数字类型。未来的语言也不应该关心类型。这些都是底层的细节，应该被屏蔽掉。 今天之所以需要关心，还是迫于实现细节或者性能妥协。

动态语言依然是未来的方向。静态型的语言做做基础工具，会被当成汇编永远活在幕后。

现在编程语言就像服装的流行元素了，翻来覆去就那几个造型，比如喇叭裤，80 年代流行了，90 年代销声匿迹了，2000 年后又流行了，现在又销声匿迹了，过几年，还会再流行一次。 这不，上个月 C++ 又在排行榜上火了一把

其实炒火一个语言（框架）的套路也很简单：
1、告诉还没入行的年轻人，学会了这个新语言你就能把前面用旧语言的老家伙拍在沙滩上
2、告诉老家伙，学会这门新技术你就不用 996 了，不用天天面对屎山了，不用被领导 pua 了，女朋友也能找到了
3、告诉各个大厂小厂，我们背后有足够的资金把这门技术炒火，有足够的能量忽悠大量的年轻的以及年老有经验的炮灰，供你们像农贸市场买菜一样挑挑拣拣。

数学非常关心数据类型，类型决定了性质，同样一个数字 1，在 mod 5 和 mod 6 的意义上是不同的，前者是域可以套用线性代数，后者就不行。所以数学里取一个数字都会写 let n ∈ N，let n ∈ Q 等等，这些就是数据类型。数学的未来反而是迁移到由更强大的类型系统支持的定理证明器上，这样才能用机器验证证明，并且构造一个可靠的数学知识库。

求教，定理证明器是干什么用的？有没有现实中应用的例子？好像很多学术语言都搞成什么 prover 了。

定理证明器能自动证明勾股定理吗。。。？纯属好奇，对这些东西没有了解。

现实中的例子就是把数学证明写成代码，然后用计算机验证。定理证明器只能通过搜索来找证明，搜索空间不会太大，因此自动并不是重点，重点只是验证。

看看 Mathematica ? 不过我好久没用了，只在大学做实验用过。MA 里面不关心类型，而且帮助数学家们推演公式。先进的数学编程语言，是自己从头实现的。python 数学库和 MA 相比是个弟弟

这些称作计算器语言更恰当，定理证明器是什么样的可以参见 https://ruby-china.org/topics/41265 或者 https://leanprover.github.io/ 。

TheoremProving

不过进入陌生领域了，Mathematica 也有定义证明。我就贴上了，这部分没做过。没有发言权了。

https://reference.wolfram.com/language/guide/TheoremProving.html

以高深莫测结束

我感觉目前 ruby-china 论坛的 Feed 流做的不够好。应该改进一波，把喜欢交流的人们再次聚合在一起分享交流，大家有什么想法？

很难，人心散了队伍难聚了

是的，现在论坛不是求职，就是吹水，然后技术贴也都是和 rails 无关的。本质就是 rails 只有已经毕业转语言的，或者多年搬砖的老手，这些人一般遇到问题都可以自己解决，没必要上论坛讨论。

其实本来这个论坛有趣的地方就是隔一段时间就会来一个人过来踢场子，说一些 ruby / rails 是傻 b 的话，现在连黑粉都没有了。唉，其实被骂也是一种幸福，黑粉也是粉。

编程语言分为两种，没人骂的和没人用的。

v 站似乎包罗万象