robturtle
commented
7 years ago 语音方面，系统编程建议把列表里的 c++ 换成 rust，函数式建议关注 idris。
在 type system 的框架下，正确性，执行效率，都只是函数的签名而已。本身这部分就该由机器来完成。一部分是计算力的提升，更关键的还是近年来PLT上方法论上的进展吧。只需要更改代码的组织形式，就能获得正确性和效率的提升。所以，在排除计算力提升的影响还能带来效益，这才是现在PLT最令人兴奋的地方。
rust 可以看作是 a better c++，mozilla 用它写了最新的 firefox 内核算是验证了可行性。未来完全可以不用去看C++那坨X了。idris 则是内嵌了自验证逻辑的 a better haskell，除了在优化方面暂时不如 haskell 以及目前还不稳定外，前景还是很好。
https://charlesliuyx.github.io/2017/10/13/%E7%A8%8B%E5%BA%8F%E5%91%98%E6%8A%80%E8%83%BD%E5%9B%BE%E8%B0%B1/