Skip to content

fix typos #18

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
ritschwumm wants to merge 1 commit into
base: master
Choose a base branch
from
Open

fix typos #18

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Whitepaper.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ that solution is that providing a semantics and, thus, proving the consistency
of the resulting system becomes extremely hard.

Aaron Stump moved on from self types towards a very similar solution based on
dependent intersections. The idea is theat, instead of relying on mutual
dependent intersections. The idea is that, instead of relying on mutual
recursion, inductive datatypes can refer to themselves in simplified, erased
forms. This results in a comparably small language that is much easier to
provide a semantics for, which Aaron Stump called Cedille-Core. In exchange,
Expand All @@ -99,7 +99,7 @@ Formality has a different take on consistency that comes from the realization
that consistency isn't hard, it is complex. The reason is that consistency
demands termination, which, due to the halting problem, simply can't be
implemented without either forbidding a program that is "important to someone",
or by making the language extremelly more complex.
or by making the language extremely more complex.

For example, there is a very easy way to make a proof language consistent:
disable recursion and non-affine lambdas. This would be sound even with
Expand Down