Old Berkeley Pascal to Free Pascal wasn't too bad. Other than clashes over new reserved words and conversion to modern I/O, that went well.

The LISP part, though, is not going well. Porting clever 1970s Stanford AI Lab macros written on the original SAIL machine to modern Common LISP is hard. Anybody with a knowledge of MACLISP want to help? The code is all on Github. If you're into this, try to convert the macros "defsmac" and "defmac" in this file [1] to clisp. Submit a pull request.

At least now both languages can do POSIX I/O. We had some implementation-specific C glue code in the original just to talk to pipes. That can go away.

Looking to the future, Dafny level verification could easily deal with two of the big unsafe areas in Rust - partially initialized arrays (used for collections that can grow), and backpointers. Those have clear invariants, easy proofs, and the proofs can be done by an automatic prover. You don't need a labor-intensive interactive system like Coq.

The Dafny approach has the nice property that it's all right there in the program source code. There's no separate verification data to be kept in sync. We did that in Pascal-F, too, but many later systems have the user working in a completely different mathematical notation for verification purposes. This is a huge turnoff for programmers.

[1] https://github.com/John-Nagle/pasv/blob/master/src/CPC4/defm...

I can't read MACLISP, but these two Common Lisp macros match the behavior that's described in the big comment:

    (defmacro defsmac (name params expr)
      `(defmacro ,name ,params
         (sublis (mapcar 'cons ',params (list ,@params)) ',expr)))
    
    (defmacro defmac (name params expr)
      `(defmacro ,name ,params
         (list '(lambda ,params ,expr) ,@params)))

Thanks very much. It turns out the first one can be called with multiple args in the "expr" slot, so it has to be

    (defmacro defsmac (name params &rest expr)
      `(defmacro ,name ,params
         `,(cons 'progn (sublis (mapcar 'cons ',params 
                (list ,@params)) ', expr))))

but your code got me un-stuck.