From 6f1f25c23cbf4ce383f70ab1cd741fd6f31c97ca Mon Sep 17 00:00:00 2001
From: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com>
Date: Wed, 26 Oct 2022 00:25:22 +0100
Subject: [PATCH] wip

---
 languages.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/languages.md b/languages.md
index 548492a..796dd30 100644
--- a/languages.md
+++ b/languages.md
@@ -16,7 +16,7 @@ Idris is a purely functional language with:
 
 Idris shares dependent types and theorem proving with Agda, but is [designed for](http://docs.idris-lang.org/en/latest/faq/faq.html#what-are-the-differences-between-agda-and-idris) general purpose programming. It is inspired by Haskell, and uses much of the same syntax. As of 2022, Idris isn't ready for production deployment.
 
-One difficulty I have noticed with Idris is that it can very difficult indeed to write performant, correct, purely functional, and provably total systems of any significant size. The effort required can reduce a developer's capacity to pay attention to quality. This negative feedback loop of correctness versus ease of use is similar to the problem that secure systems can require a complicated UI, but a complicated UI is a security hazard because users can be tempted to circumvent protocols.
+One difficulty I have noticed with Idris is that it can very difficult indeed to write performant, correct, purely functional, and provably total systems of any significant size. The effort required can reduce a developer's capacity to pay attention to quality. This negative feedback loop of correctness versus ease of use is similar to the problem in security that secure systems can require a complicated UI, but a complicated UI is a security hazard because users can be tempted to circumvent protocols.
 
 ### [Rust](https://www.rust-lang.org/)