diff --git a/README.md b/README.md index 312c1e6..9fca0bc 100644 --- a/README.md +++ b/README.md @@ -29,11 +29,11 @@ Simplicity introduces a groundbreaking low-level programming language and machin The distinguishing aspects that set Simplicity apart from conventional programming languages are: - **Distinct Programming Paradigm**: Simplicity's programming model requires a paradigm shift from conventional programming. It hinges on reasoning about programs in a functional sense with a focus on combinators. This intricacy surpasses even popular functional languages like Haskell, with its own unique challenges. -- **Exceptional Low-Level Nature**: Unlike high-level languages such as JavaScript or Python, Simplicity operates at an extremely low level, resembling assembly languages. This design choice enables easier reasoning about the formal semantics of programs, but is really work on directly. +- **Exceptional Low-Level Nature**: Unlike high-level languages such as JavaScript or Python, Simplicity operates at an extremely low level, resembling assembly languages. This design choice enables easier reasoning about the formal semantics of programs, but is rarely worked on directly. ## SimplicityHL -SimplicityHL is a high-level language that compiles to Simplicity. It maps programming concepts from Simplicity onto programming concepts that developers are more familar with. In particular, Rust is a popular language whose functional aspects fit Simplicity well. SimplicityHL aims to closely resemble Rust. +SimplicityHL is a high-level language that compiles to Simplicity. It maps programming concepts from Simplicity onto programming concepts that developers are more familiar with. In particular, Rust is a popular language whose functional aspects fit Simplicity well. SimplicityHL aims to closely resemble Rust. Just how Rust is compiled to assembly language, SimplicityHL is compiled to Simplicity. Just how writing Rust doesn't necessarily produce the most efficient assembly, writing SimplicityHL doesn't necessarily produce the most efficient Simplicity code. The compilers try to optimize the target code they produce, but manually written target code can be more efficient. On the other hand, a compiled language is much easier to read, write and reason about. Assembly is meant to be consumed by machines while Rust is meant to be consumed by humans. Simplicity is meant to be consumed by Bitcoin full nodes while SimplicityHL is meant to be consumed by Bitcoin developers. diff --git a/book/src/function.md b/book/src/function.md index 92588be..7d41c2a 100644 --- a/book/src/function.md +++ b/book/src/function.md @@ -22,7 +22,7 @@ The function then checks if the carry is true, signaling an overflow, in which c On the last line, the value of `sum` is returned. The above function is called by writing its name `add` followed by a list of arguments `(40, 2)`. -Each parameter needs an argument, so the list of arguments is as long as the list of arguments. +Each parameter needs an argument, so the list of arguments is as long as the list of parameters. Here, `x` is assigned the value `40` and `y` is assigned the value `2`. ```rust @@ -54,7 +54,7 @@ fn level_1() -> u32 { } fn level_2() -> u32 { - let (_, next) = jet::increment_32(level_1)); + let (_, next) = jet::increment_32(level_1()); next } ``` @@ -91,7 +91,7 @@ There is no support for "libraries". ## Jets -Jets are predefined and optimized functions for common usecases. +Jets are predefined and optimized functions for common use cases. ```rust jet::add_32(40, 2) diff --git a/book/src/let_statement.md b/book/src/let_statement.md index 70c9d1c..0950953 100644 --- a/book/src/let_statement.md +++ b/book/src/let_statement.md @@ -48,7 +48,7 @@ let z: u32 = { assert!(jet::eq_32(y, 2)); // y == 2 x }; -assert!(jet::eq_32(x, 3)); // z == 3 +assert!(jet::eq_32(z, 3)); // z == 3 ``` ## Pattern matching diff --git a/book/src/type.md b/book/src/type.md index 4f0295f..faf7f48 100644 --- a/book/src/type.md +++ b/book/src/type.md @@ -100,11 +100,11 @@ Arrays are always of finite length. | `List` | <256-list | `list![]`, …, `list![a1, …, a255]` | | `List` | <512-list | `list![]`, …, `list![a1, …, a511]` | | … | … | … | -| `ListN`>` | <2N-list | `list![]`, …, `list![a1, …, a`(2N - 1)`]` | +| `List` | <2^N-list | `list![]`, …, `list![a1, …, a_{2^N - 1}]` | Lists hold a variable number of elements of the same type. This is similar to [Rust vectors](https://doc.rust-lang.org/std/vec/struct.Vec.html), but SimplicityHL doesn't have a heap. -In SimplicityHL, lists exists on the stack, which is why the maximum list length is bounded. +In SimplicityHL, lists exist on the stack, which is why the maximum list length is bounded. <2-lists hold fewer than 2 elements, so zero or one element. <4-lists hold fewer than 4 elements, so zero to three elements. @@ -156,7 +156,7 @@ Sum types represent values that are of some "left" type in some cases and that a [They work just like in the either crate](https://docs.rs/either/latest/either/enum.Either.html). [The Result type from Rust is very similar, too](https://doc.rust-lang.org/std/result/index.html). -A sum type type is generic over two types, `A` and `B`. +A sum type is generic over two types, `A` and `B`. The value `Left(a)` contains an inner value `a` of type `A`. The value `Right(b)` contains an inner value `b` of type `B`. diff --git a/book/src/type_casting.md b/book/src/type_casting.md index eb4d2e9..ba4d10d 100644 --- a/book/src/type_casting.md +++ b/book/src/type_casting.md @@ -57,7 +57,7 @@ All casting in SimplicityHL happens explicitly through a casting expression. ``` The above expression casts the value `input` of type `Input` into some output type. -The input type of the cast is explict while the output type is implicit. +The input type of the cast is explicit while the output type is implicit. In SimplicityHL, the output type of every expression is known. @@ -78,4 +78,4 @@ let x: u32 = <(u16, u16)>::into((0, 1)); ``` In the above example, we cast the tuple `(0, 1)` of type `(u16, u16)` into type `u32`. -Feel free to consult the table above to verify that this is valid cast. +Feel free to consult the table above to verify that this is a valid cast. diff --git a/doc/environment.md b/doc/environment.md index 3c72cb9..ebd97e8 100644 --- a/doc/environment.md +++ b/doc/environment.md @@ -22,7 +22,7 @@ During the translation, we can ignore the source type of Simplicity expressions Target types are handled by contexts. -We obtain context Ctx(Ξ) from environment Ξ by mapping each variable `a` from Ξ to the target type of Ξ(`x`): +We obtain context Ctx(Ξ) from environment Ξ by mapping each variable `x` from Ξ to the target type of Ξ(`x`): Ctx(Ξ)(`x`) = B if Ξ(`x`) = a: A → B @@ -37,7 +37,7 @@ As we translate `s` to Simplicity, we need an environment that maps the variable If `p` is just a variable `p = a`, then the environment is simply [`a` ↦ iden: A → A]. -If `p` is a product of two variables `p = (a, b)`, then the environment is [`a` ↦ take iden: A × B → A, `b` ↦ drop iden: A × B → B. +If `p` is a product of two variables `p = (a, b)`, then the environment is [`a` ↦ take iden: A × B → A, `b` ↦ drop iden: A × B → B]. "take" and "drop" are added as we go deeper in the product hierarchy. The pattern `_` is ignored. diff --git a/doc/translation.md b/doc/translation.md index 077228e..66d76b3 100644 --- a/doc/translation.md +++ b/doc/translation.md @@ -78,7 +78,7 @@ Then ⟦`b; c`⟧Ξ = comp (pair ⟦`b`⟧Ξ ⟦`c`⟧Ξ) (drop iden): A → C If Ctx(Ξ) ⊩ `b`: B -If Product(PEnv(B, `p`), Ξ) ⊩ c: C +If Product(PEnv(B, `p`), Ξ) ⊩ `c`: C Then ⟦`let p: B = b; c`⟧Ξ = comp (pair ⟦`b`⟧Ξ iden) ⟦`c`⟧Product(PEnv(B, `p`), Ξ): A → C @@ -90,7 +90,7 @@ If Product(PEnv(B, `x`), Ξ) ⊩ `b`: D If Product(PEnv(C, `y`), Ξ) ⊩ `c`: D -Then ⟦`match a { Left(x) => a, Right(y) => b, }`⟧Ξ = comp (pair ⟦a⟧Ξ iden) (case ⟦b⟧Product(PEnv(B, `x`), Ξ) ⟦c⟧Product(PEnv(C, `y`), Ξ)): A → D +Then ⟦`match a { Left(x) => b, Right(y) => c, }`⟧Ξ = comp (pair ⟦`a`⟧Ξ iden) (case ⟦`b`⟧Product(PEnv(B, `x`), Ξ) ⟦`c`⟧Product(PEnv(C, `y`), Ξ)): A → D ## Left unwrap