From 1ad372ccc3f48f24b1e48517f7b8df5316af6168 Mon Sep 17 00:00:00 2001 From: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com> Date: Wed, 26 Oct 2022 00:11:04 +0100 Subject: [PATCH 1/8] add comment on complexity and capacity --- languages.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/languages.md b/languages.md index 755f933..3a9632a 100644 --- a/languages.md +++ b/languages.md @@ -17,6 +17,8 @@ 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, but is written in C. As of 2021, 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 a significant size. The effort required can reduce a developer's capacity to pay attention to quality, in much the same way that a complicated UI is a security hazard because users can be tempted to circumvent protocols. + ### [Rust](https://www.rust-lang.org/) Rust gives the performance and memory profile of C, while guaranteeing memory and thread safety. It achieves this with an ownership memory model and its type system. It is often spoken of as having a steep learning curve, but I don't think this opinion is always justified. It simply enforces the rules you _should_ learn in languages like C, but might not. Moreover, there are a number of ways of explicitly trading performance or safety for syntactic and conceptual simplicity. From d4153bd8252212d7b9de6c93e739c464a040c7fa Mon Sep 17 00:00:00 2001 From: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com> Date: Wed, 26 Oct 2022 00:15:29 +0100 Subject: [PATCH 2/8] fix comment re Idris written in C --- languages.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/languages.md b/languages.md index 3a9632a..ea14c9b 100644 --- a/languages.md +++ b/languages.md @@ -15,7 +15,7 @@ Idris is a purely functional language with: * theorem proving, which allows one to guarantee certain properties of runtime values at compile time, such as an integer being within some bounds -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, but is written in C. As of 2021, Idris isn't ready for production deployment. +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 2021, 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 a significant size. The effort required can reduce a developer's capacity to pay attention to quality, in much the same way that a complicated UI is a security hazard because users can be tempted to circumvent protocols. From 13c8370ba587ad1b66d4dbf0ac2ed1acc7e79139 Mon Sep 17 00:00:00 2001 From: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com> Date: Wed, 26 Oct 2022 00:15:50 +0100 Subject: [PATCH 3/8] wip --- languages.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/languages.md b/languages.md index ea14c9b..f187b19 100644 --- a/languages.md +++ b/languages.md @@ -15,7 +15,7 @@ Idris is a purely functional language with: * theorem proving, which allows one to guarantee certain properties of runtime values at compile time, such as an integer being within some bounds -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 2021, Idris isn't ready for production deployment. +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 a significant size. The effort required can reduce a developer's capacity to pay attention to quality, in much the same way that a complicated UI is a security hazard because users can be tempted to circumvent protocols. From 57c3f82f469c929e04a34efe46ee9154f422888b Mon Sep 17 00:00:00 2001 From: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com> Date: Wed, 26 Oct 2022 00:20:52 +0100 Subject: [PATCH 4/8] wip --- languages.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/languages.md b/languages.md index f187b19..5b390b6 100644 --- a/languages.md +++ b/languages.md @@ -12,8 +12,7 @@ Idris is a purely functional language with: type * quantitative types, where you can specify how many of a value exist at runtime. This can be used to erase values at runtime, or ensure only one reference exists to a unique physical entity - * theorem proving, which allows one to guarantee certain properties of runtime values at compile - time, such as an integer being within some bounds + * theorem proving, which allows one to guarantee certain properties of functionality, such as the reverse of a list is its own inverse 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. From 337d44254c3e3c953098359c5b06161830d0fdd8 Mon Sep 17 00:00:00 2001 From: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com> Date: Wed, 26 Oct 2022 00:21:20 +0100 Subject: [PATCH 5/8] wip --- languages.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/languages.md b/languages.md index 5b390b6..cdb3a6d 100644 --- a/languages.md +++ b/languages.md @@ -12,7 +12,7 @@ Idris is a purely functional language with: type * quantitative types, where you can specify how many of a value exist at runtime. This can be used to erase values at runtime, or ensure only one reference exists to a unique physical entity - * theorem proving, which allows one to guarantee certain properties of functionality, such as the reverse of a list is its own inverse + * theorem proving, which allows one to guarantee certain properties of functionality, such as the reverse of a list being its own inverse 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. From ac5290fea0e6357cf9f9c374bb8f6ed380ec8590 Mon Sep 17 00:00:00 2001 From: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com> Date: Wed, 26 Oct 2022 00:22:04 +0100 Subject: [PATCH 6/8] wip --- languages.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/languages.md b/languages.md index cdb3a6d..9e54ccf 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 a significant size. The effort required can reduce a developer's capacity to pay attention to quality, in much the same way that 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, in much the same way that a complicated UI is a security hazard because users can be tempted to circumvent protocols. ### [Rust](https://www.rust-lang.org/) From c9d80c9aa4252a41e8cf5c1c036ac1773da9c6bb Mon Sep 17 00:00:00 2001 From: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com> Date: Wed, 26 Oct 2022 00:24:37 +0100 Subject: [PATCH 7/8] wip --- languages.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/languages.md b/languages.md index 9e54ccf..548492a 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, in much the same way that 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 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/) From be6fc4278c403a4817400489549dd23e1c3ac289 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 8/8] 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/)