AI 编程是否会带来强类型语言的普及？ AI 写的 JS，如果是冷门一点的库经常弄错参数， IDE 没报错运行也不一定能发现

[zxkmm]

AI 写的某段代码好不好，和强类型弱类型没有关系。AI 根本不知道代码是什么意思，代码写的不好就说明 AI 预训练的不好。

[lekai63]

强类型一般而言 有利于 IDE 的提示。

我认为：最好是编译型语言，AI 写完后，相当于 IDE 能帮忙直接检查错误。 尽量避免运行后才发现，会导致一个个改 很痛苦。

[cmdOptionKana]

现代化 IDE 发展起来之后，新语言就很少是动态类型的了，而且动态类型也开始加 type hint ，这些转变都与 AI 无关，别啥都往 AI 上扯。

[drymonfidelia]

@zxkmm 但是如果没有类型，人检查不出错误
@lekai63 冷门库文档不全，AI 无法理解怎么用才是对的

[kingme]

先用 ai 帮你把冷门的库转成 ts

[echo1937]

只要还需要 人类介入，强类型就有优势，原因#3 楼说了。

如果不需要人类介入，什么类型其实没差别，甚至编程语言都会有革新。

[boxrq]

@lekai63 #2 rust

[Xerxes2]

@boxrq 但是我测试过哪怕是吹的最厉害的 sonnet 3.7 写的 Rust 都非常蠢，一个简单问题来来回回改四五次浪费我钱。

[boxrq]

@Xerxes2 #8 哈哈，感觉有两点原因，第一个是 rust 还是太新了，市面上优秀的语料远不如其他语言多，第二个 rust 本身复杂性也高。但是这条路感觉是一条很不错的路，ai 和编译器去打架，人主要关注业务。等 ai 再进化一下

[drymonfidelia]

@kingme 不现实，我让 cursor 把我一个加起来 500 行代码的小项目转成 ts ，一堆问题，修了 10 次都没成功，还没我手动快

[charles0]

我设想中的编程语言不仅要强类型+静态类型，还要有一定的形式化验证能力和依赖类型，像 Dafny 语言、Idris 语言和 Ada/SPARK 语言那样尽可能静态地保证程序的正确性，让 AI 在编写代码的同时还编写证明。目前看来经过合适的训练以后 AI 可以编写证明过程，参考 DeepMind 的 AlphaGeometry 项目解决的几何证明题。现有的形式化验证项目如 seL4 和 CompCert 最大的问题是一行普通代码可能对应十几行证明，开发效率太低，如果能用 AI 的话可能可以大大加快对关键基础设施开源项目的形式化验证。目前我想到的最大问题还是语料不足和 AI 成本比较高。

[riceball]

这是专业知识问题，需要外挂专业专家知识库，掌握这些知识一般人都容易会被误导，更别说 AI.一旦涉及到深入，都需要各行业的专家的支持，互联网的信息最多趋同的，往往并不准确。

比如 js,现在你问 AI,JS 的 ES6 的 class 是增强了 js 的特性，还是削弱了 js 的特性？大都会认为是增强而不是削弱。