有没有任何可以证明的现实世界语言？ （Scala呢？） [英] Are there any provable real-world languages? (scala?)
问题描述
我曾在大学教过正式系统，但我很失望，他们没有似乎被用在了真实的单词中。
我喜欢能够知道某些代码（对象，函数，其他）能够工作的想法，而不是通过测试，但通过 proof 。
我确定我们都熟悉物理工程和软件工程之间不存在的相似之处（钢行为可预见，软件可以做任何事 - 谁知道！），我很想知道是否有任何语言可以用在真正的单词中（要求Web框架太多以至于无法提出要求？）
我听说过像scala这样的功能性语言的可测试性的有趣事情。
$ b 作为软件工程师我们有什么选择？
是的，有些语言可以编写可证明的corr ect软件。有些甚至用于工业。 Spark Ada 可能是最显着的例子。我曾与Praxis Critical Systems Limited的几个人谈过，他们使用它在Boings上运行代码（用于引擎监控），看起来相当不错。 （这是一个很棒的该语言的摘要/描述）。该语言和伴随的证明系统使用下面描述的第二种技术。它甚至不支持动态内存分配！
我的印象和经验是，有两种技术可以编写正确的软件：技巧1：用您熟悉的语言（例如C，C ++或Java）编写软件。 如果你的抱负是100％正确的（这通常是汽车/航空航天工业中的一项要求） ）你会花费很少的时间编程，并有更多的时间证明。 技术2：用稍微笨拙的语言编写软件（Ada的一些子集或者例如OCaml的调整版本），并且一路写下正确性证明。这里编程和验证齐头并进。 Coq编程甚至完全等同于它们！ （请参阅咖喱霍华德对应）
在这些情况下，你总是会得到一个正确的程序。 （一个错误将被保证植根于规范中）。您可能会花更多时间进行编程，但另一方面，您在此过程中证明它是正确的。
请注意，这两种方法都取决于您手边有正式规范的事实（您将如何判断正确/不正确的行为），以及正式定义语言的语义（你还能怎么知道程序的实际行为）。
以下是一些正式方法的例子。如果它是现实世界，取决于你问谁： - ）
- Coq定理证明者：用Coq编程（技巧2）
- ESC / Java （技巧1，尽管声音也不完整） >
- Spec＃（技巧1，既不是声音和完整虽然）
- 为什么/ Krakatoa （技术2，基于Java）
我知道只有一个证明正确的网络应用程序语言： UR 。 通过编译器的Ur程序保证不会：
- 遭受任何类型的代码注入攻击 >
- 返回无效HTML
- 包含死链内应用程序链接
- HTML表单与其预期的字段之间存在不匹配处理程序
- 包含客户端代码，这些代码对远程Web服务器提供的AJAX风格的服务进行了不正确的假设
- 尝试无效的SQL查询
- 在SQL数据库或浏览器与Web服务器之间使用不正确的封送处理或反编组
I was taught about formal systems at university, but I was disappointed how they didn't seem to be used in the real word.
I like the idea of being able to know that some code (object, function, whatever) works, not by testing, but by proof.
I'm sure we're all familiar with the parallels that don't exist between physical engineering and software engineering (steel behaves predictably, software can do anything - who knows!), and I would love to know if there are any languages that can be use in the real word (is asking for a web framework too much to ask?)
I've heard interesting things about the testability of functional languages like scala.
As software engineers what options do we have?
Yes, there are languages designed for writing provably correct software. Some are even used in industry. Spark Ada is probably the most prominent example. I've talked to a few people at Praxis Critical Systems Limited who used it for code running on Boings (for engine monitoring) and it seems quite nice. (Here is a great summary / description of the language.) This language and accompanying proof system uses the second technique described below. It doesn't even support dynamic memory allocation!
My impression and experience is that there are two techniques for writing correct software:
Technique 1: Write the software in a language you're comfortable with (C, C++ or Java for instance). Take a formal specification of such language, and prove your program correct.
If your ambition is to be 100% correct (which is most often a requirement in automobile / aerospace industry) you'd be spending little time programming, and more time proving.
Technique 2: Write the software in a slightly more awkward language (some subset of Ada or tweaked version of OCaml for instance) and write the correctness proof along the way. Here programming and proving goes hand in hand. Programming in Coq even equates them completely! (See the Curry-Howard correspondence)
In these scenarios you'll always end up with a correct program. (A bug will be guaranteed to be rooted in the specification.) You'll be likely to spend more time on programming but on the other hand you're proving it correct along the way.
Note that both approaches hinges on the fact you have a formal specification at hand (how else would you tell what is correct / incorrect behavior), and a formally defined semantics of the language (how else would you be able to tell what the actual behavior of your program is).
Here are a few more examples of formal approaches. If it's "real-world" or not, depends on who you ask :-)
- The Coq Theorem Prover: Programming with Coq (technique 2)
- ESC/Java (technique 1, neither sound nor complete though)
- Spec# (technique 1, neither sound nor complete though)
- Why / Krakatoa (technique 2, based on Java)
I know of only one "provably correct" web-application language: UR. A Ur-program that "goes through the compiler" is guaranteed not to:
- Suffer from any kinds of code-injection attacks
- Return invalid HTML
- Contain dead intra-application links
- Have mismatches between HTML forms and the fields expected by their handlers
- Include client-side code that makes incorrect assumptions about the "AJAX"-style services that the remote web server provides
- Attempt invalid SQL queries
- Use improper marshaling or unmarshaling in communication with SQL databases or between browsers and web servers
这篇关于有没有任何可以证明的现实世界语言？ （Scala呢？）的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
