圆桌派 | TauChain创始人Ohad：图灵完整框架本质上是不安全的

Q

Yuki

链读品牌负责人

A

Ohad Asor

TauChain创始人

12月27日晚8点，我们第二期AMA嘉宾邀请到了TauChain创始人Ohad Asor。

Ohad是一名数学家及软件开发者，自1995年起工作于以色列一家高科技公司。他曾经是以色列最年轻的大学生，主修数学和计算机科学。学习和工作期间，Ohad在计算机和数学领域学习了大量的知识，积累了丰富的经验，近几年还对逻辑学，机器学习，复杂性理论，科学哲学，经济学，社会选择（social choice），以及去中心化网络进行了深入的研究。他设计实施了Tau和Agoras项目。作为创始人，Ohad领导整个项目的开发。

Tauchain一个特点是形式化验证，所以语言设计是非图灵完备。这种形式化验证和基于coq类实现的形式化验证相比有何设计上的不同？本期我们的主题是《形式化验证：Tau语言VS图灵完备，看看Ohad怎么说？》，为你解答更多Tauchain细节。

请简要介绍一下什么是Tau？

Tau是一个完全由其用户完全有效地限定的p2p网络。因此我们必须提出一个以便许多用户能够共同决定下一个Tau的区块（或“自动更新”）决策过程。

Tau 主要想解决的问题是什么？

大规模决策问题通常通过投票来解决，就像议会选举一样。 但是这种方式存在一个大问题：每个人都有平等的投票权，但并不是每个人都拥有提出所需投票提案的平等权利。 这源于一个现实问题：人们如何在一天时间内阅读成千上万的提案。

这个问题不仅影响到了用户治理P2P网络的情况，更涉及到大部分人的决策过程。传统的投票解决方案也在p2p空间中出现过，例如 Tezos的研究成果不允许在提案，讨论和投票过程中产生的大量信息广泛传播，并且所有应当被考虑的问题都会被简化为相对较少的信息。当然这也是实际一些原因导致的。

Tau提供哪种投票选择？

我们试图通过将大规模的决策问题转化成一些小规模的决策过程，从而来解决上述实际问题。 在小团体中，我们不需要投票。 我们表达我们的想法，意见仅来自我们所说的内容，并且无需任何投票程序即可清晰地传达给所有人。即使涉及许多人参与的大规模讨论中，只要计算机可以“理解”人们的观点，并由此创建观点结构图并以此来计算得出共识结论。

因此我们设计了一种决策机制，在该机制中用户以机器可以理解的某种语言写出他们的观点（将在后面进行解释），然后计算机系统计算归纳出他们的正面或反面观点，并根据用户的共识进行不断转变更新。

您所提到的“机器可以理解的语言”是什么意思？

对于要在系统上使用的语言，请允许我引用文章“ The New Tau”：

我们认为不应该也不能仅仅只有一种通用语言。 因为没有一种语言可以很好的满足所有需求。 因此我们提出了一种能够定义新语言的元语言，但是这与将回到一种通用的[元]语言相一致。因此我们要求元语言能够重新定义自己并并不断自我迭代，就像它可以定义其他语言一样。这样我们不仅获得了多种语言，而且获得了一种自我修正的语言，这是自我修正系统中的重要组成部分。

事实证明可以自我定义并具有良好逻辑特性（如可判定性）的逻辑并不常见。即使我们有通用的图灵机，但也很难找到表达能力更强、信息量更大（例如，可判定的）的语言。 我们采用了PFP逻辑，从有限模型理论书中可以看出PFP逻辑的传递信息能力是完全PSPACE的，并且在1999年的imhof中“能够自我定于语义的逻辑”被证明可以自我定义。

从这里我们继续谈论互联网语言。我们使用的元语言被称为TML（Tau Meta-Language，可以从github上正在进行的程序中获得记忆），元语言用户通过指定逻辑公式来描述新语言，这些逻辑公式展示了用两种不同语言的描述不同文档具有相同含义。换句话说，要定义一种新的语言，需要保证它如何将原有语义翻译转换为现有语言。我们所指的语义是语言描述的本体（对象和关系），而不是编程语言中的操作语义。这样我们就获得了传递知识语言的相互联系，进而使得语言的选择无关紧要。可以将一种语言的文档（使用TML程序）转变为不同的语言。

我们已经强调我们tau完全不处理自然语言分析。当然从理论上讲，也许有一天某人将通过TML进行编程使得其能完全理解自然语言，但我们并不指望这种事情的发生。事实上确实有许多自然语言的形式主义都已经非常接近完整的自然语言，这也便于人们去使用（我们指的是“机器可以理解的足够简单的英语”），因此在某种程度上我们可以期望TML处理人类可理解的语言，但是现在TML还旨在用于仅机器语言。例如，人们可能想将文档转换为格式化的HTML或Wiki，或者将某种高级语言的程序转换为机器代码，或者从逻辑中合成代码。

因此互联网语言将允许多种语言在系统中随时间共存和发展。为了在网络进行讨论用户将使用这些语言，并在机器理解了所讲内容的前提下享受机器增强讨论的能力。

Tau的逻辑框架有何特别之处？

为了能够合理且协同地做出影响整个系统的决策，我们提出了“三个规则中的规则”，这是任何语言规则的三个基本要求（国家，组织或法规，或者p2p网络的规则）：

1.对于任何X来说，我们要求始终在有限的时间内回答“是否X合法”问题。换句话说，我们要求这个问题是可确定的。

2.语言必须允许自我参照，因为法律通常是指“法律”，尤其是涉及到需要更改法律的法律时。（有关更多详细信息，请参见文章“自参考的艺术”）

3.最低要求是有能力去更改法律，例如在我们要制定与旧法律相抵触的新法律的情况下。

前两个要求很少会结合在一起。事实证明，TML不仅满足元语言的要求，而且满足这三个法律定律。

因此，Tau专门用于满足这些要求的非常具体的逻辑框架。这样的框架在描述复杂性和有限模型理论领域称为FO [PFP]。

去中心化网络中合作决策模式是如何制定的？

除了产生社会选择机制的逻辑框架外，我们还考虑了p2p网络的设置，这限制了协作决策能力，这主要是由于无法唯一标识用户。这样一来，攻击者可能无需采取其他措施，就能影响网络的行为，如中国谚语所说：“如果错误的人使用了正确的工具，那么正确的工具就会以错误的方式发挥作用”。有关在电子分散式环境中决策的更多信息，请参见文章“共识和选择”。

Agoras的主要特征有哪些？

Agoras将成为一种货币，它不仅将由Tau技术提供动力，还将由其用户管理，还将具有以下特征：

1.知识市场：纯知识-现金交易，在文章“从 Agoras到TML”中介绍，

2. 具有无风险利息，而不印刷新硬币的，先进的衍生品市场，这在文章“共识和选择”中描述。

3. 计算资源市场，其中的想法是描述在Zennet，但当然事情将适应Tau框架。

Tauchain什么时候主网上线，之前有计划2019年完成TML和Alpha Tau的开发，现在开发到哪步？

我们几乎完成了TML和Alpha：TML已经准备好支持初始Alpha，并且已经满足了介绍中提到的所有公理，但是要使TML达到其最终目标：成为正式语言之间编写翻译的工具，作为语言互联网设计的一部分，还有更多工作要做。Alpha目前正在开发中，我们即将发布一些非常初步的内容。自上个月以来，我们的开发团队已经从一个人增加到了六个人。因此，我们期望发展会更快。此外，几乎所有的困难部分已经完成。

对于主网，很难给出估计。事情可能会如此快速和成功，并且我们将在一年内完成所有工作。

Tauchain与以太坊的区别是什么？为什么觉得图灵完整性本质上是不安全的？

以太坊是一种支持智能合约的货币，与之前介绍的Tau的目标有很大不同。

图灵完整框架本质上是不安全的，因为本质上不可能回答有关程序行为的所有问题。例如，我们想询问该程序是否会做我们不希望做的事情，或者询问它是否执行了我们希望执行的计算。在图灵完整的框架中，不能保证所有程序都能回答此类问题。这样一来，只要我们不将自己限制在图灵不完整的语言上，就无法在任何情况下知道程序将执行的功能。

Tauchain一个特点是形式化验证，所以语言设计是非图灵完备，这种形式化验证和基于coq类实现的形式化验证相比有何设计上的不同? TauChain的形式化验证是基于什么计算机理论开发的？

Coq和类似证明很通用，并且支持多种逻辑。我们的范围适用于满足上述法律定律的逻辑。通过这种方式，例如，我们可以拥有一个全自动的证明器，而Coq和类似的证明器则需要用户干预。Tau逻辑背后的理论在第5题已予论述。

人们认为TauChain与Tezos有类似的特征。两者都是self-amendment blockchain，两者的智能合约语言都具有形式化验证的功能。能否说明一下TauChain与Tezos的区别？

正如法律法则所描述的，我们要求网络规则必须用可判定的语言来书写。Tezos不支持可判定性，但图灵已完成。此外，Tezos的社会选择机制是基于投票，投票不能公平地拓展，正如我们在前面的答案所表明的。

Tauchain自身是不需要代币的，agrs只是上面一个应用的代币，这种经济模型上的设计是否会不利于Tauchain。Tau团队只占令牌总供应量的3％，出于什么考虑？

确实，Agoras需要Tau，但是tau并不在技术上依靠agoras。但是，在存在知识市场的情况下，Tauchain上的知识可以发展得更好。保持网络运行（如矿工）的激励措施也很重要，并且需要某种形式的价值。

我们之所以只保留3％（我们考虑再三）的原因是，我们清楚整个事情会变得有多大。如果我们真的相信，我们没有理由保留更多令牌。

花絮

   lory

众所周知，目前的区块链项目通常至少具有共识结构。也许我可以假设这不是区块链项目，或者你重组了“区块链”？

Axe   

那么在tauchain上建立dapp，例如微信，最初的版本只需要用tau开发的非常接近自然语言的语言来''discuss''即可，以后便会自我升级？

  空谷

为什么图灵是完全框架不安全？是否有更详细的讨论呢？只给出一个清晰场景的例子。

  空谷

以我的理解，在TauChain上写代码本质上是一个有代码的建议。既然是建议，那么相应的治理模型是如何实现的呢？

江南梅Ethan(一航)   

tauchain是很底层的技术，是一个开发工具与运行平台，是一张可以画任何东西的白纸+一只笔，所以灵活性很强。

  Miaomiao

试问真有个系统能从无数人的无数意见统计，推理，值多少？从这些意见自动编代码，值多少？

然‘谈论’从5人左右就开始降效，扩大到百万人，对社会发明新知识的效率的印象，值多少？等

徐生   

只讨论技术，偏执；只讨论价钱，偏执；不论研究的是什么，ama的多么透彻，目的就一个:抱着鸡蛋变凤凰。

  空谷

治理上，Tau 的底层逻辑是，如果有一种语言能够表达出每个人的心声和意志，那么使用这种语言的治理系统就能够非常高效地达成共识（且不论结果是好是坏）。

举个英国脱欧为例，如果这个语言能够精准地识别到大部分人只是投脱欧的票着玩，并不想真正脱欧，那么这个系统最终达成的共识可能就是不脱欧。所以大家可以看到，在脱欧这个场景下，纯投票能够表达的意志太少了，换句话说就是投票这种治理工具的意图表达力太弱了。所以需要表达力更强的治理工具。

大家都这么厉害，还有我主持人啥事……

21点开始了自由讨论环节，链读圆桌派群里，技术大佬瞬间活跃起来。Ohad也非常慷慨地说：“我会一直在这里，解答大家的问题。”

群里有来自各个技术社区的大佬，有项目投资负责人，大家就TauChain的目标、技术进展、难题，展开讨论。

Ohad，22点30结束AMA解答。RChain与TauChain社群技术大佬就TauChain的目标、技术可行性、进展，进一步展开讨论。一边是质疑，一边是解惑，技术切磋一直持续到半夜2点半……

应群友要求，链读圆桌派AMA火药味升级，将召集天下技术项目，前来battle。今起，“链读圆桌派AMA”正式改名为“链读圆桌派AMA 华山论链”。这里提供一个公正的平台，邀您学术共鸣。

编辑 / Yuki

链读推荐