What do language designers do to decide or prove that a particular feature works correctly?

Question

I'm interested in language design and in general I can reason easily about widely known features (e.g. inheritance, polymorphism, delegates, lambdas, captures, garbage collection, exceptions, generics, variance, reflection, and so on), their interactions in a particular language, the ways they can possibly be implemented, their limitations, etc.

In the last few months, I started reading about Rust, which has an ownership system that ensures memory safety and deterministic resource management by forcing object lifetimes to be statically verifiable. From the perspective of a plain user of the language, I could pick up the system almost immediately.

From the perspective of a language designer, however, it took me a while to realize why things in Rust are exactly the way they are. I couldn't immediately understand the reasoning behind some restrictions of the ownership system, until I forced myself to come up with cases that would violate the integrity of a system if it didn't have those aspects.

My main question has nothing to do with Rust and its ownership specifically -- but feel free to use it as an example in your comments/answers, if you need to.

When language designers design a new feature, what methodology or process do they use to decide that the feature works properly?

By "new" I mean that it's not something that has already been tested in existing languages (and thus the bulk of the work has been done by other designers). By "works properly" I mean that the feature solves the intended problem correctly, and it's reasonably bulletproof. By "reasonably bulletproof" I mean that no code can be written in the language or a particular subset of the language (e.g. a subset without "unsafe" code) that would violate the integrity of the feature.

• Is it a trial and error process, in the sense that you come up with a simple form of the feature, then try to find ways to violate it, then patch it if you successfully violate it, then repeat? And then, when you can't think of any other possible violations, you hope there's nothing left and call it a day?

• Or is there a formal way to actually prove (in the mathematical sense of the word) that your feature works and then use that proof to confidently get the feature right (or mostly right) from the start?

(I should mention that I have an engineering background, not computer science. So if I'm missing something that would be obvious to CS people, please feel free to point it out.)

Answer 1

I'm having trouble finding the exact reference at the moment, but a while ago I watched several videos by Simon Peyton Jones, who was a major contributor to Haskell's design. He is an excellent speaker on type theory, language design, and the like, by the way, and has many videos available for free on youtube.

Haskell has an intermediate representation which is essentially lambda calculus augmented with a few simple things to make it easier to work with. Lambda calculus has been used and proven since a computer was just a person who computed things. An interesting point Simon Peyton Jones makes often is that whenever they do something wild and crazy with the language, he knows it's fundamentally sound when it eventually reduces back down to that intermediate language.

Other languages are not nearly so rigorous, instead favoring ease of use or implementation. They do the same things other programmers do to get high quality code: follow good coding practices and test it to death. A feature like Rust's ownership semantics I'm sure gets both a lot of formal analysis and testing to find forgotten corner cases. Often features like that start out as someone's graduate thesis.

Answer 2

So for language design, there are proofs (or bugs). For example, type systems. Types and Programming Languages is the canonical book describing type systems, and focuses on proving the correctness and completeness of the type system. Grammars have similar analysis, and algorithms (like the ownership system you describe) have their own.

For language implementation, it is code like any other. You write unit tests. You write integration tests. You do code reviews.

The only thing that makes languages special is that they are (almost always) infinite. You literally cannot test for all inputs. And (ideally) they are used by tons of people, doing weird and interesting things, so any bug in the language will be found eventually.

Practically, relatively few languages use proofs to verify their functionality, and end up with some mixture of the options you mention.

Answer 3

The first and most difficult thing a language designer must take care of when introducing new features, is to keep his language consistent:

• how can it be integrated in the language grammar without breaking existing code (this can be mathematically proven)
• how it relates with existing features (for example if you have fixed arrays indexed 0..n-1, you will not introduce a new variable array feature indexed 1..n) (that's the artistic part of the design)
• how the feature can be implemented accross the whole toolchain so that the new feature can be absorbed by the ecosystem, the toolmakers and the programmers (the feasbility can be demonstrated with a proof of concept, but full implementation is an approach similar to programming)

To guide in this matter, a designer relies on a set of design rules and principles. This approach is very well described in "The design and evolution of C++" from Bjarne Stroustrup, one of the rare books dedicated to language design. What is very interesting is to see that languages are rarely designed in a vacuum, and designer look also how their languages have implemented similar features. Another source (online and free) is the design principles for the java language.

If you look at public proceedings of standardization committees, you'll see that it is more a trial error process. Here an example on C++ module a fully new concept to be introduced in the next version of the language. And here an analysis drafted after some language changes, to assess its success. And here the Java Community Process to define new Java specifications, such as a new api. You will see that this work is performed by several experts who draft creatively a concept paper and a first proposal. Then these proposals are reviewed by a larger community/committee which may amend the proposal to ensure a higher degree of consistency.

Answer 4

How to test programming language features? It's a very good question, and I'm not sure that the state of the art is up to the job.

Each new feature can interact with all the other features. (This affects the language, docs, compilers, error messages, IDEs, libraries, etc.) Do features combine to open up a loophole? To create nasty edge cases?

Even very smart language designers working hard to maintain type soundness discover violations such as this Rust bug. Rust's type system is not so obvious to me but I think in this case having the type system track value lifetimes means lifetime "subtyping" (subranges) clashes with expectations for ordinary subtyping, coercions, references, and mutability, creating a loophole where a static lifetime ref can point to a stack-allocated value and later become a dangling reference.

By "works properly" I mean that the feature solves the intended problem correctly, and it's reasonably bulletproof.

For languages intended to be production languages, that is, used by many programmers to build reliable production software, "works properly" must further mean solving the intended problem correctly for the intended audience.

In other words, usability is as important to language design as it is to other kinds of design. This entails (1) design for usability (e.g. knowing your audience), and (2) usability testing.

An example article on this topic is “Programmers are People, Too, Programming language and API designers can learn a lot from the field of human-factors design.”

An example SE question on this topic is Has the syntax of any programming language been usability tested?

An example usability test considered extending a list-iteration feature (I don't remember which language) to take multiple lists. Did people expect it to iterate through the lists in parallel or through the cross-product? The language designers were surprised by the usability test findings.

Languages like Smalltalk, Python, and Dart were designed with an emphasis on usability. Clearly Haskell was not.