• m2_720345
  • 791.4KB
  • zip
  • 0
  • VIP专享
  • 0
  • 2022-06-04 01:03
具有正式证明的现代编程语言。 现在自己写! 为什么要正式证明? 当大多数人听到形式证明时,他们自然会想到数学和安全性,或“无聊的东西”。 虽然可以使用形式化证明来正式化定理并验证软件的正确性,但Formality的方法却有所不同:我们专注于将证明用作提高开发人员生产率的工具。 毫无疑问,将类型添加到非类型化语言中可以大大提高生产率,特别是当代码库增长到一定程度时:只需看看TypeScript的兴起。 形式证明在某种程度上是通用语言中使用的简单类型的演变。 我们认为,证明是等待探索的超级大国,正确使用证明可以以破坏性的方式提高开发人员的生产力:想想Haskell在类固醇上的骇客。 正式性旨在探索和启用形式证明的这一方面,我们将在不久后发布更多有关形式证明的信息。 为什么要正式? 市场上有一些有趣的证明语言或通常称为的证明助手。 , , , 等。 但是这些(在某些情况下,也许除我
![[alt text]](blog/img/formality-banner-white.png ) A modern programming language featuring formal proofs. Now written in itself! Why formal proofs? ------------------ When most people hear about formal proofs, they naturally think about mathematics and security, or, "boring stuff". While it is true that formal proofs can be used to formalize theorems and verify software correctness, Formality's approach is different: we focus on using proofs as a tool to **enhance developer productivity**. There is little doubt left that adding types to untyped languages greatly increases productivity, specially when the codebase grows past a certain point: just see the surge of TypeScript. Formal proofs are, in a way, an evolution of the simple types used in common languages. We believe that proofs are superpowers waiting to be explored, and the proper usage of them can enhance the productivity of a developer in a disruptive manner: think of Haskell's Hackage on steroids. Formality was designed to explore and enable that side of formal proofs, and we'll be publishing more about that soon. Why Formality? -------------- There are some interesting proof languages, or proof assistants, as they're often called, in the market. [Agda], [Coq], [Lean], [Idris], to name a few. But these (perhaps with exception of Idris, which we love!) aren't aligned with the vision highlighted above, in some key aspects: ### Auditability Formality is entirely compiled to a small [trusted core] that has 700 lines of code. This is 1 to 2 orders of magnitude smaller than existing alternatives. Because of that, auditing Formality is much easier, decreasing the need for trust and solving the "who verifies that the verifier" problem. ### Portability Being compiled to such a small core also allows Formality to be easily compiled to multiple targets, making it very portable. For example, our [Formality-to-Haskell] compiler was developed in an evening and has less than 1000 lines of code. This allows Formality to be used as a a lazy, pure functional language that is compiled directly by Haskell's GHC. ### Performance Formality has a long-term approach to performance: make the language fast in theory, then build great compilers for each specific target. Our [JavaScript compiler], for example, is tuned to generate small, fast JS, allowing Formality to be used for web development. Other targets may have different optimizations, and we're constantly researching new ways of evaluating functional programs; see our post about interaction nets and optimal reduction ([Absal]). [trusted core]: https://github.com/moonad/formcorejs [Formality-to-Haskell]: https://github.com/moonad/FormCoreJS/blob/master/FmcToHs.js [formality.js]: https://github.com/moonad/FormalityFM/blob/master/bin/js/src/formality.js [Agda]: https://github.com/agda/agda [Idris]: https://github.com/idris-lang/Idris-dev [Coq]: https://github.com/coq/coq [Lean]: https://github.com/leanprover/lean [Absal]: https://medium.com/@maiavictor/solving-the-mystery-behind-abstract-algorithms-magical-optimizations-144225164b07 [JavaScript compiler]:https://github.com/moonad/FormCoreJS/blob/master/FmcToJs.js ### Market Readiness For a programming language to be used in real-world applications, it must satisfy certain minimal requirements. It must have a great package manager, a good editor, friendly error messages, a fast compiler and a clear, non-cryptic syntax that everyone can use and understand. All of these are non-goals for some of the existing alternatives, but are high priorities for Formality. Usage ----- [![formality-js](https://img.shields.io/npm/v/formality-js)](https://www.npmjs.com/package/formality-js) 1. Install Using the JavaScript release (`fmjs`): ```bash npm i -g formality-js ``` Using the Haskell release (uses `fmhs` instead of `fmjs`): ```bash git clone https://github.com/moonad/formality cd formality/bin/hs cabal build cabal install ``` 2. Clone the base libraries ```bash git clone https://github.com/moonad/formality cd formality/src ``` 3. Edit, check and run Edit `Main.fm` on `formality/src` to add your code: ```c Main: IO(Unit) do IO { IO.print("Hello, world!") } ``` Type-check to see errors and goals: ```bash fmjs Main.fm ``` Run to see results: ```bash fmjs Main --run ``` Since Formality doesn't have a module system yet, you must be at `formality/src` to use the base types (lists, strings, etc.). In this early phase, we'd like all the development to be contained in that directory. Feel encouraged to send your programs and proofs as a PR! Quick Introduction ------------------ ### A simple, clear, and unsurprising syntax > If you can't explain it simply, you don't understand it well enough. Why make it hard? Formality aims to frame advanced concepts in ways that everyone can understand. For example, if you ask a Haskeller to sum a list of positive ints (Nats), they might write: ```c sum(list: List(Nat)): Nat case list { nil : 0 cons : list.head + sum(list.tail) } Main: IO(Unit) do IO { IO.print("Sum is: " | Nat.show(sum([1, 2, 3]))) } ``` Or, if they are enlightened enough: ```c sum(list: List(Nat)): Nat List.fold<_>(list)<_>(0, Nat.add) Main: IO(Unit) do IO { IO.print("Sum is: " | Nat.show(sum([1, 2, 3]))) } ``` But, while recursion and folds are nice, this is fine too: ```c sum(list: List(Nat)): Nat let sum = 0 for x in list: sum = x + sum sum ``` The code above isn't impure, Formality translates loops to pure folds. It is just written in a way that is more familiar to some. Proof languages are already hard enough, so why make syntax yet another obstacle? *(You can test the examples above by editing `Main.fm`, and typing `fmjs Main.fm` and `fmjs Main --run` on the `Formality/src` directory.)* ### Powerful types Let's now see how to write structures with increasingly complex types. Below is the simple list, a "variant type" with two constructors, one for the `empty` list, and one to `push` a positive number (`Nat`) to another list: ```c // NatList is a linked list of Nats type NatList { empty push(head: Nat, tail: NatList) } ``` As usual, we can make it **more generic** with polymorphic types: ```c // List is a linked list of A's (for any type A) type List (A: Type) { empty push(head: A, tail: List(A)) } ``` But we can make it **more specific** with indexed types: ```c // Vector is a linked list of Nats with a statically known size type Vector ~ (len: Nat) { empty ~ (len: 0) push(len: Nat, head: Nat, tail: Vector(len)) ~ (len: 1 + len) } ``` The type above isn't of a *fixed length* list, but of one that has a length that is *statically known*. The difference is that we can still grow and shrink it, but we can't, for example, get the `head` of an empty list. For example: ```c Main: IO(Unit) def list = [1,2,3] def vect = Vector.from_list<Nat>(list) def head = Vector.head<Nat,_>(vect) do IO { IO.print("First is: " | Nat.show(head)) } ``` Works fine, but, if you change the list to be empty, it will result in a type error! This is in contrast to Haskell, where `head []` results in a runtime crash. **Formality programs can't crash. Ever!** *(You can also check the program above by editing `Main.fm`.)* ### Theorem proving Proof languages go beyond checking lengths though. Everything you can think of can be statically verified by the type system. With subset types, written as `{x: A} -> B(x)`, you can restrict a type arbitrarily. For example, here we use subsets to represent even numbers: ```c // An "EvenNat" is a Nat `x`, such that `(x % 2) == 0` EvenNat: Type {x: Nat} (x % 2) == 0 six_as_even: EvenNat 6 ~ refl ``` This program only type-checks because `6` is even: try changing it to `7` and it will be a type error! Bu