Add soundness and completeness to glossary #54
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
MaloJaffre
reviewed
Feb 13, 2018
src/glossary.md
Outdated
| @@ -7,6 +7,7 @@ Term | Meaning | |||
| ------------------------|-------- | |||
| AST | the abstract syntax tree produced by the syntax crate; reflects user syntax very closely. | |||
| codegen unit | when we produce LLVM IR, we group the Rust code into a number of codegen units. Each of these units is processed by LLVM independently from one another, enabling parallelism. They are also the unit of incremental re-use. | |||
| completeness | soundness is a technical term in type theory. Completeness means that every type-safe program also type-checks. Having both soundness and completeness is very hard, and usually soundness is more important. (see "soundness"). | |||
MaloJaffre
reviewed
Feb 13, 2018
| @@ -25,6 +26,7 @@ provider | the function that executes a query ([see more](query. | |||
| query | perhaps some sub-computation during compilation ([see more](query.html)) | |||
| sess | the compiler session, which stores global data used throughout compilation | |||
| side tables | because the AST and HIR are immutable once created, we often carry extra information about them in the form of hashtables, indexed by the id of a particular node. | |||
| soundness | soundness is a technical term in type theory. Roughly, if a type system is sound, then if a program type-checks, it is type-safe; i.e. I can never (in safe rust) force a value into a variable of the wrong type. (see "completeness"). | |||
There was a problem hiding this comment.
Sorry, what is the typo here?
There was a problem hiding this comment.
Oops sorry, I wrongly read this sentence.
|
@mark-i-m Thanks, lgtm! I will have to pick up some book on type theory at some point this year, though 👍 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
See #48
cc @phansch