1. 20

  2. 25

    While no WASM expert, I don’t think the stuff about WASM is justified: I don’t see any relationship between WASM and LISP.

    First, WASM having a textual assembly format based on S-expressions doesn’t mean WASM is related to LISP. S-expressions are to LISP as JSON is to JavaScript – they’re a language-neutral way of expressing a tree structure in text. WASM itself is a series of binary instructions, like other real or virtual instruction sets, AFAIK.

    Second, re. “Formal verifiers - behind the scenes - then will ensure, that everything uploaded (by customers) will precisely follow its predefined specifications” — bytecode verifiers just check a minimal set of correctness, like that the code won’t make illegal branches or reads/writes, or underflow the stack. The JVM has been doing this for 25 years. It doesn’t prove a program will behave as intended, just that it won’t crash in particular ways nor produce undefined behavior.

    (I am aware that there are algorithms for proving correctness of [very small] programs, and I’m sure analyzing program correctness is easier in a homomorphic language like LISP; I’m just responding to the claims about WASM.)

    1. 9

      Yeah exactly, he’s confusing syntax for semantics. WASM has a 32-bit flat address space… Lisp has a garbage collected heap of dynamically typed cells. WASM has only four types i32, i64, f32, f64, and all functions take and return those types.

      They’re not even close in their programming model.

      1. 15

        I also find it funny that PicoLisp is being touted in a safety context. This is a language that segfaults when you try to evaluate a symbol that isn’t a function. It’s an impressive language, but it has fewer rails than most.

        1. 1

          Lisps do exist without garbage collection.

          According to pico lisp’s creator, it only has one data type (section 2.2).

          1. 3

            PicoLisp still has GC, even with just one data type, because that data type is effectively a tagged union of pointers, a string-esque thing, numbers, and cons cells. (4 type bits, each for one type)

        2. 7

          The key question when anyone talks about formal verification is to ask what properties they’re verifying. If they don’t state this up front, they’re probably trying to sell you snake oil. Even if they do, you need to look at them carefully. A couple of examples I’ve seen where this was important:

          We have some formally verified code that guarantees spatial and temporal memory safety. Temporal safety was expressed (oversimplifying slightly) with the invariant that no access to an object happened after a free of that object. It turned out that the verification of temporal safety was passing because of a degenerate case of this: no object was ever freed. The code was correct according to the properties that were verified, it’s just that no one expressed ‘all allocated objects are freed’ in the specification (and, once they did, expressing when they were freed was quite complicated).

          A while ago, I came across a formally verified kernel where they guaranteed forward progress. They made a big deal of this. It turns out that they did it by having no preemption while in the kernel and all system calls were able to spuriously fail if they couldn’t complete immediately. For example, on most *NIX systems, dup needs to lock the file descriptor table. This can block, so instead this kernel allowed their dup system call to fail with EAGAIN and the userspace wrapper had to retry. Because there was no coordination between userspace callers, userspace threads had weaker forward progress guarantees than on existing operating systems (two userspace threads repeatedly calling dup could prevent each other from making forward progress).

          1. 3

            Yeah, this is a hell of a leap. There are s-expressions used in wasm, but they’re used in a very different way from how lisps use them.

            This is like saying “my project uses bencode, which is the encoding format used by bittorrent; I picked it because bittorrent is really good for distributed peer-to-peer data.”

            1. 2

              I guess I’d have to disagree with you.

              Quoting from Practical Common Lisp:

              A typical division is to split the processor into three phases, each of which feeds into the next … In Common Lisp things are sliced up a bit differently, with consequences for both the implementer and for how the language is defined. Instead of a single black box that goes from text to program behavior in one step, Common Lisp defines two black boxes, one that translates text into Lisp objects and another that implements the semantics of the language in terms of those objects

              S-expressions are thus essential to Lisp. They are what allows lisp to be both code and data at the same time.

              Quoting from Wikipedia:

              Thus, Lisp programs can manipulate source code as a data structure, giving rise to the macro systems that allow programmers to create new syntax or new domain-specific languages embedded in Lisp.

              The interchangeability of code and data gives Lisp its instantly recognizable syntax. All program code is written as s-expressions, or parenthesized lists.

              To be my own Devil’s advocate, no, not all S-expressions are valid Lisp, but to suggest that

              S-expressions are to LISP as JSON is to JavaScript

              really undersells how vital sexps are to Lisp.

              1. 7

                IIRC The importance of S-expressions was a discovery. Initially they were not regarded as the holy grail as many of us do now. The initial LISP paper has M-expressions for code and S-expressions for internal compiler stuff.

                I love S-expressions as well, and I’ve made a stupid toy language that runs on Racket, generates WASM textual representation and then compiles it using the WASM tools. The S-expressions in WASM textual representation are just a prettier way to do a form of improved assembly, they are not lispy (unless you add a preprocessor and go crazy with macros, then it can get lispy quite fast).

                1. 4

                  That’s correct. My point was that S-expressions are not LISP, and using S-expressions as an intermediate representation does not make something LISPy.