From 17a3516584b542a327e59d19fa42ee6763a25719 Mon Sep 17 00:00:00 2001 From: Andrew Yu Date: Sat, 15 Jan 2022 21:58:09 +0800 Subject: quotes direction --- index.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'index.html') diff --git a/index.html b/index.html index 3b1cded..673d756 100644 --- a/index.html +++ b/index.html @@ -44,7 +44,7 @@

A Lisp-like Operating System

Anybody who has tried functional programming knows that Lisp and Haskell are special and great programming languages. Most Lispers and all Haskell programmers adhere to the functional style of programming, creating mathematically-provably-correct programs. I love the fact that Haskell supports Monads well and that it's statically typed (having the debugger find your issues is much more comfortable than debugging mid-run, while it's true that GHC has quite good debugging utilities. On the other hand, Haskell and Common Lisp have so many pragmatics and syntax sugar. Scheme (which I consider to be a dialect of Lisp) is much more uniform and symmetric (think of group theory) in syntax, but has bad support for lazy evaluation.

There are many modern operating systems, for example the BSDs, GNU+Linux, Plan 9, etc. (Microsoft Windows and macOS don't count, they're nonfree.) But security issues are discovered every year in each of them, even OpenBSD, which is considered the most secure operating system for general use. A lot of this has to do with the programming language they're written in, C.

-

In C, you've got a heap of pointers, memory stacks, arrays, linked lists, structures, etc. that you all have to manage by yourself. This leaves huge gaps for programmer error. By contrast, it is possible to mathematically prove the correctness (or the lack thereof, though I only use "Possible" because of Godel Incompleteness) of a functional program. This eases the work for programmers.

+

In C, you've got a heap of pointers, memory stacks, arrays, linked lists, structures, etc. that you all have to manage by yourself. This leaves huge gaps for programmer error. By contrast, it is possible to mathematically prove the correctness (or the lack thereof, though I only use “Possible” because of Godel Incompleteness) of a functional program. This eases the work for programmers.

Most, if not all security issues in programs written in classical imperative programming languages are with bogus stacks, pointers, etc. There are countless times when stack overflows are used in attacks. By using functional languages, it just works!

There have been great proposals by other people on this ideea. If you are into operating system development and programming in general, please read it, and share your thoughts with me. If many people voice on this issue, I'll start an mailing list.

What about a pure functional Lisp dialect, with monads and similar (Haskell) ideas?

@@ -78,7 +78,7 @@
-- cgit 1.4.1-2-gfad0