编译型语言的下一步改进会是什么? 已翻译 41%

漆兴 投递于 2017/08/21 17:35 (共 17 段)
阅读 368
收藏 0
0
加载中

最近,斯蒂芬妮·赫尔伯特 (Stephanie Hurlburt) 在推特上表示,对于在计算机行业工作了一段时间的人来说,接受陌生人的“观众提问”是有益健康的。我答应了,有人问了我一个有趣的问题:

“在内存安全之后,您认为编译语言的下一步是什么?”

撇开“编译”语言在相当长一段时间内具有各种或多或少可信的“内存安全”这一事实不谈,我同意(显然!)将内存安全作为所有语言设计领域(尤其是系统语言)的桌面筹码;但是还有很多事情要做!所以我想我应该花点时间来详细说明一些我们仍然很不理想的领域;也许一些未来的语言工程师可以从这些笔记中找到灵感。

翻译于 2018/10/28 08:43
0

在继续之前,我要强调的是:这些是个人和主观的想法,对此我并不是特别感兴趣(因此,除非你确实有建设性的东西可以补充,否则不要在评论中进行辩论);互联网上的人对这些话题都很感兴趣,坦率地说,我有点厌倦了人们对这些话题的热情程度。此外,这些意见并不代表我的雇主的意见。这是我在业余时间写的个人博客。苹果有一种很好的,很扎实的语言,我很乐意为之工作,这种沉思与此无关。我相信 Swift 代表了主流技术的重大进步,正如我在发布时所说的那样。

所有这些都表明,用其他语言来描述未来会是什么样子? 

翻译于 2018/10/28 08:45
0

广泛适用的问题领域

这些要么是无处不在的抽象概念,要么是仍然需要工作的问题,就我所知基本上需要在任何主流语言下继续研究。

模块

这听起来可能有些奇怪,但是大多数语言都有严重缺陷的模块系统。我同意 Bob Harper 关于模块最重要的评价。许多语言根本就没有模块系统,而许多只有一个模块系统的语言只能作为管理名称空间或编译顺序的一种方式。更强大的模块系统存在——你会遇到一些如果你曾与依赖的组件类型,类类型,特征,签名,仿函数,但有一系列令人眼花缭乱的设计约束导航(繁殖,透明度,分层,连贯性,子类型化,higher-order-ness,first-class-ness,单独编译,可扩展性,递归)来到达一个实用,可用的模块系统。几乎没有一种语言能以足够令人信服的方式做到这一点,以至于我认为问题已经解决。目前该领域的领先研究可能是 Andreas Rossberg 关于 1ML 的研究。但是如果你要探索这个领域的话,有几十年的基础工作需要你认真阅读。

翻译于 2018/10/28 08:50
0

(写这篇文章让我觉得它需要一个脚注/警告:如果在阅读这些评论时,你觉得模块 - -或者我在这里要提到的任何其他内容 -- 都是一件容易理解的“简单的事情”,且是显而易见的正确答案,我觉得你可能会感染斯德哥尔摩综合症,这恰恰是由于你目前最喜欢的语言,工程师综合症,和/或Dunning-Kruger效应而综合产生的。真的有许多技术娴熟的人穷其一生挣扎着反对这些问题,并且每个运输系统都有严重的问题,他们根本没有正确处理。)

错误

这也可能更像是一个惊喜,通常说来任何语言中,我不相信我们已经“解决”错误管理。我们有一些可靠的设计-哲学学派,大多能够很好地结合语言:代数效果和处理程序,检查和未检查的异常,分区和监督树崩溃失败,monad,结果总和类型,条件/重启系统,回滚交易;但是没有一个能够完全解决设计空间,使问题似乎已经“解决”。甚至承诺一个又一个这样的制度 - -它不但涉及一些机制,而且涉及一整套支持错误管理的连锁协议 - -几乎每种已知方法都存在严重的抽象泄漏和设计权衡(模块化,组合性,局部性,同步性,健全性,认知负荷,实施成本,不同制度的界面成本)。错误是非常难以处理的。

蜗牛伊
翻译于 2018/12/10 09:39
0

Daira Hopwood在工作中的Noether语言上有一些注释和设计材料,我们还需阅读很多其他东西才能继续向前推进。这些内容将带你开启漫长的旅程,既有很多挑剔的技术材料,也有许多高度主观的,彻头彻尾的哲学话题,比如“如何保护自己免于错误”和“对或错的价值到底意味着什么“。

协同,async/await,“用户可见”异步性

目前流行的是新语言有async/await之类的东西。这并不意味着是优秀的解决方案:一些问题已经解决,但很多仍然是一团糟。同步世界和异步世界之间的界限 - 在类型,控制流,正确性,错误,模块性,组合方面 - 仍然非常尴尬。在不同的同步体制之间,特别是在FFI或不同的运行时间之间,是否需要缓和以及如何缓和,这很难。最后的效果整合很难。与并行性的集成很难。哪些部分需要语言支持很难,哪些部件面向用户很难。认知负荷仍然很高。

蜗牛伊
翻译于 2018/12/10 11:03
0

效果系统,更一般地说

在何处以及如何将效果集成到主流编译语言中,这些仍然没有达成一致的共识。 类型系统研究范围似究似乎已经超越了这一点,现在能轻易地说“类型和效果系统”,似乎它们已经解决了问题; 但大多数语言中的程序员都没有接触到任何有意义的效果系统,更不用说最先进的,可扩展的,强推理的系统。 像EffKoka这样的语言在未来主流方向上处于领先地位,但它仍远未成为主流,需要解决很多问题:模块化,多态性和编码等等,与特征的一般认知负荷一样。

扩展静态检查(ESC),细化类型,一般依赖类型语言

对比哥斯拉电影的重新制作,几十年的语言设计更频繁,这是因为它本质上是不错的理念,只是在设计空间方面非常困难。

蜗牛伊
翻译于 2018/12/12 10:21
0

我们的想法是在你的类型系统中嵌入一个“逻辑”(边界在形式上并不是真的存在,但在概念上和认知上肯定是!)这样用户可以定期自由地融合他们使用的类型以及其他“逻辑类型”,前者能够确定数据和函数的内存形状,后者能够断言那些数据和函数的通用性,(半)计算的谓词类。换句话说,让用户以完整的(也就是说,原始递归的)表达语言编写程序的“一般”正确性条件,并让“类型系统”静态检查(证明)那些条件(或者发出显示反例的错误消息,就像类型错误一样)。

这些系统离“完全成熟”的高阶依赖型理论证明助手la Isabelle,Coq,Lean等还有些差距;虽然在某些情况下类型系统在相同的区域内。设计问题取决于注释负担足够低,用户才不会沮丧地放弃:像大多数类型的系统一样,用户总是必须为系统提供一些信息以推断其余部分,但是当更具表现力的逻辑出现时,平衡就会明显地倾斜,朝着“太多注释”的方向发展。许多情况下,注释的规模超过了被注释的程序,并且这些注释的维护负担(当用户编辑程序时)大于编码负担。作为一名语言设计师,这并不是一个好的用户体验。

蜗牛伊
翻译于 2018/12/12 10:47
0

到目前为止,此领域的大多数实践都以令人沮丧的方式告终,或者在故障成本高的领域(强调安全的嵌入式系统等)应用有限。比起ESC,大多数主流语言肯定更多......呃,可判定系统类型,精简输入或依赖型语言项目已经提出。但这并不意味着死路一条。这意味着(如果你坚定信念,我就是)一个尚未拥有突破性产品的设计空间!手机就是这样。也许再过十年或二十年,我们将回顾这些无聊类型的黑暗时代。

这个领域的项目在其类型系统中具有一定程度的表达能力(达到它们统一“逻辑”和“类型”的程度),也涉及到从研究测试平台到主流可行性尝试的范围;我觉得没有资格(不是指这里)做一个详细的比较和对比工作,所以我只是转储一些链接。如果你想进入这个领域,你至少应该学习Sage,Stardust,Whiley,Frama-C,SPARK-2014,Dafny,F *,ATS,Xanadu,Idris,Zombie-Trellys,Dependent HaskellLiquid Haskell

一旦你踏足这个区域,请做好准备:这些复杂性在其他计算机区域看起来......有点像孩子的游戏。它非常密集,非常快。这之类的东西读起来就像有关计算机人如何编写数学书籍的漫画?

蜗牛伊
翻译于 2018/12/14 15:27
0

Actual Formalization / Metatheory

Speaking of formal logic: an unfortunate fact about most languages -- even simple ones with very pedestrian type systems -- is that they usually ship with next-to-no formalization of their semantics, nor proofs that any such formalizations have any interesting metatheoretic properties (eg. soundness). We tend to just make do with testing and informal, whiteboard-and-email level reasoning about the systems, hoping that'll get us close enough to correct that it'll be ok.

This approach is, to say the least, wearing thin. Compilers still have serious bugs decades after they ship, failing to implement the languages they're supposed to. Worse, languages in the field still have serious design flaws decades after they ship, failing to uphold safety properties when subject to formal analysis. Long term, we have to get to the point where we ship languages -- and implementations -- with strong, proven foundations. There are promising moves in this direction, both in designed-for-language-designer tools like K framework or Redex, and in the general set of libraries and projects being undertaken in general proof assistants like Isabelle and Coq.

还没有人翻译此段落
我来翻译

Grab bag of potential extras for mainstream languages

These are issues with (IMO) potential applicability to mainstream languages, but I think a little less clear of a foundational role in structuring the language; a little more like "features it'd be nice to include in the design". Some have come and gone before, others are still in research form.

Session types, behavioural types, choreographies

There's a family of work called Behavioural Types, Session Types or Choreographies, that involve describing the possible interaction traces of both sides, or all sides, of a multi-party interaction, into a single "global type" -- the type of the interaction itself -- and then systematically refining / decomposing that type into a set of separate but dual endpoint-types, that each enforce only-legal-transitions (in sending, recieving and state-changing senses) on the participants.

There are various ways to encode this idea in a language, and lots of components; people have done encodings and experiments, even some prototype languages (eg. Links and Scribble), but nothing that's broken through to the mainstream yet. But I think it's a very promising area that's not too hard to understand. Lots of minable papers, good potential return on investment for taking the research mainstream.

还没有人翻译此段落
我来翻译
本文中的所有译文仅用于学习和交流目的,转载请务必注明文章译者、出处、和本文链接。
我们的翻译工作遵照 CC 协议,如果我们的工作有侵犯到您的权益,请及时联系我们。
加载中

评论(0)

返回顶部
顶部