I'm not sure what you mean by monotonicity. I don't think I rely on that. Here's how I used to see Rust until this thread:
- First comes the calculus, i.e. a grammar and operational semantics for programs. There is no notion of unsafe here, no lifetimes, no types, just low-level code. In particular, because there are no types, traits inference and other type-directed code generation is already resolved.
- Then comes the compiler, i.e. a function from Rust calculus to a Target calculus preserving a notion of behavior (usually some bisimulation). Because there are many ways to translate preserving behavior, compilers usually optimize to select the "best" target program (according to some user-chosen criteria like
-O3or-Oz). Note that there are no types yet, compilers optimize a priori with their own whole program analysis (which doesn't work for dynamic libraries and requires LTO for static libraries). This is the most precise information they can get. - Comes the type system, i.e. a grammar and semantics for types, and typing rules for programs. Types classify programs and usually exclude "bad" programs. Typing rules preserve this semantics. Programmers use type checkers to avoid some manual proofs (usually this is all manual proofs, but in Rust this is just some of them). At this stage comes unsafe and lifetimes into play. There's 2 usage of unsafe: in expressions (e.g. unsafe blocks) to mark parts of the program containing manual proofs, and in types (e.g. unsafe functions) to extend the semantics of types (e.g.
[unsafe fn(T) -> S] ⊇ [fn (T) -> S]) which can then be refined through documentation. Note that here comes type-directed code generation into play too. - Because type systems are whole-program analyses and compilers are also programs, compilers themselves can be optimized by using type information to optimize faster and better. This of course requires that type information is correct (i.e. if
phas typeTthenp ∈ [T].opt). This also enables library optimization without LTO because types are a contract that communicates whole-program analysis information through the different parts of a program.
In all of this, no monotonicity was used. Programs have a well-defined operational semantics. It is possible to extend the calculus with new constructs but their semantics shouldn't change the semantics of previous programs not using the new constructs. (If one really wants to change the semantics of an existing construct, they just introduce a new one and deprecate the old, forcing users to migrate their code.) Types have well-defined semantics too (with typ = val = opt). There is no wiggle room. It is possible to extend the type system with new types and this won't change the semantics of existing types. (Similarly to programs, to change the semantics of an existing type, a new one may be added deprecating the old one.) Unlike for programs, because types are sets of programs, they naturally come with a notion of sub-typing. As such, new types naturally interact with old types. This permits to migrate at a lower cost.
Now, why is this not somehow restrictive? It is, like all type systems. You might not find the right type for your program such that it type checks. But I think, this is where Rust shines. The unsafe capability of the type systems allows exactly that: if a program doesn't type check although it should (i.e. it is not a "bad" program), the user may lower some types, add documentation, and manually prove the typing rules side conditions. However, this is still somehow restrictive (which is why so much Rust code uses &mut T instead of *mut T). If there are not enough types to chose from (i.e. the type lattice has coarse granularity), then the required documentation and manual proofs might be too big and the user will just rewrite the program differently (like in other programming languages) or just use the wrong types (like now). This is why for my vision to work it is critical to regularly add new types to the lattice as usage demands it (like NonNull<T>, Pin<&mut T>, etc).
A few reasons why I believe current Rust differs from the Rust I describe are:
- Rust designed safe Rust before unsafe Rust. It should be the opposite (safe Rust is a particular subset of unsafe Rust where proofs are automatisable and automated). This is the same as API design. Library authors should first design their unsafe API (i.e. their real API), then derive their safe API from it (for users who prefer to avoid manual proofs to the price of not being able to write some programs).
- Rust got massive adoption before providing tools (e.g. Stacked Borrows) to reject programs that are not well-typed (including manual proofs, i.e. unsafe). So ill-typed programs spread uncontrolled and now it is hard to break those programs, so the type system is modified with
typ ≠ valto make those ill-typed programs well-typed. - Rust needs a good sub-typing story (included bounded sub-typing) such that it is easy to switch between low and high level types, otherwise users won't do it.