There is another shitstorm around Rust – the just announced meme-effort to verify approximately 7500 unstafe functions in the Rust standard library.

First of all, what a joke! I never thought there are that many of em. It is easily more than the whole SML, Ocaml and Haskell standard libraries combined. Or at least of the same order.

If we want, however, to put memes aside for a while, the way to safety begins with the proper and sound principles, so the “unsoundness bugs” will never appear again.

The most fundamental principle is of a physical partition (or of a necessary distance) which usually represent an actual abstraction barrier.

The code has to be clearly partitioned at all levels. This is an old idea, and it goes back even to hardware, with the read-only segments, and what not.

There is a simple (but well-thought) proposal, lets call it hypothetically, Rust 3000.

First, the most fundamental and the most important semantic notions has to be clearly expressed in code (syntactic forms).

  • procedures has to have its distinct keyword proc. This clearly signals and communicates that this is a procedure, NOT a function. fn is cool but stupid.
  • (and this is the most important) an imperative assignment (to a location in memory) has to have the proper symbol :=. This is a warning signal.
  • functions has to have its distinct keyword func. This is a referential-transparent function, and the compiler has to prove it.

We also need to clearly distinguish between pure expressions and imperative statements. Stylistically, using and ! at the end of the commands would be the best. But… The second-best solution is a forced UPERCASE for the imperative crap. This will pay a lot in the long run.

In short, what ISN’T a math should never look like a math. Most of the confusion comes from this, and idiotic terminology, which goes all the way back to the C and the 70s, when they call imperative procedures “functions” just for fun.

Another great discovery is to capitalize type-names and the corresponding constructors and to use these symbols as “tags” for structural pattern-matching. There is a lot of subtlety why this feels and seems so right. Believe me, this is just the right thing to do (tagging and structural pattern-matching has been discovered by molecular biology itself).

If these ideas reminds one of Ada, then yes, these guys thought this out long ago.

One more time. The clear semantic distinction at all levels, starting from clear syntax, is the way to non-bullshit soundness.

Another idea is that, perhaps, at the intermediate language level, within the compiler, imperative code has to have a distinct monad-like abstraction barrier. The amazing trick which keeps Haskell pure (reverentially transparent) has to be re-used everywhere. MS did a lot of the right things in their F#.

Right now Rust is a PHP (or Ethereum) – lots of ambitions, virtue-signalling and excitement, but lack of proper education and understanding of the principles.

Math is a candle (which will help to dispel the darkness of ignorance), as Philip Wadler used to say from the stage so many times. Separating math from an imperative crap (which to some extend all mostly-functional languages did) is the fist required step to a real soundness.

Imperative “DSL”

Seemingly obvious language designs – a pure languages with all the advancements of the last 50 years (basically Haskell and F#) – data-constructors as tags, structural pattern-matching, parameterized type-classes (with kinded type-constructors).

All the curly braces has to be removed from the pure expressions and pattern-matching syntacticforms (everything is an expression and an immutable binding, of course). Functions has to have clauses (like Erlang, SML) to “match” the underlying algebraic sum-types.

Within this language we should have an embedded imperative “DSL”, based on stripped to a bare minimum oh so familiar legacy C/C++/Java idioms.

Something similar has been done before more than once – CLOS within Common Lisp, imperative constructs and the OO-subset within Ocaml. and the do-blocks in Haskell, of course.

Let them never forget all the idiotic decisions of the C legacy which almost all imperative languages are so attached to. Less emotionally, there is sort of an imperative C-tradition, which should be re-used.

  • fucking curly braces everywhere
  • fucking semicolons everywhere
  • explicit return statements
  • if is a statement
  • c-like structs
  • classes based on structs
  • procs as methods

Intentionally no expressions in these imperative curly-braced blocks, no advanced constructs, no pattern-matching, nothing. Common parts of the C/C++/Java/Javascript syntax.

A truly Modern Language

Lets just finally part with the C legacy and itstraditional syntax and re-use some results of the last 50 years of active PL research in the FP realm.

First there are a couple of emergent principles (spelled out as maxims):

  • One wants to program at a highest possible (and the most general level of abstraction, with rare occasional dives into a representation (with a DSL).

  • If one has to write a type in a user-facing code it is a low-level,archaic language. Some type-inference works even for the fucking C++

  • There should be more than one (ideally – layered) DSLs within a language (like in Common Lisp) or Haskell (which has embedded DSL for the typescript.

    Yes, it is that simple. Whole OSes were programmed in Common Lisp and it was good.

    Types should have its own DSL, with syntax that favors what should be expressed. (Haskell, including pattern-matching and the syntax of Lists).

    Yes, one has to express product types with ,, sum-types with a | and function types with an arrow ->. There are a lot behind these symbols.

Just like we have an impl blocks we could have an repr blocks, when we want to specify the memory layout for a particular algebraic type.

We do not use redundant parenthesis or curly braces anywhere. Parentheses are for nesting and priorities, again, just like ML family of languages have discovered.

Currying is not just cool, it is necessary. Having functional parameters in parenthesis is just a C legacy.

Lazy evaluation is not an optional academic curiosity – nesting (and only nesting) defines an actual order of evaluation. It is not just shortcircuiting of an if.

Writing types above the function is better than squeezing them into a single line. Try to realize this.

The : syntax for types is better because it is more uniform and can be used after any expression (yes, ML again).

Even strings and numbers can be overloaded (Haskell) so we don’t have to write stupid suffixes.

To summarize: Syntax matters a lot (do not listen to the idiots). It suggests and hints to an underlying mathematical structures. The language must be as high-level as possible, with embedded DSLs for types and for low-level stuff. Do not try to fit everything into a single syntax. Types must be inferred and occasionally hinted (specified). We do not have to write them, especially 2 times 2 times. Tools will show them.

Machine types can be nicely modeled as a bounded subsets. This has been done in CLU and Ada long time ago verynicely. The problem is that modern “language designers” do not know their field.