- Principal type-schemes for functional programs∗ Luis Damas† and Robin Milner First published in POPL ’82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM, pp. 207–212
- THE PRINCIPAL TYPE-SCHEME OF AN OBJECT IN COMBINATORY LOGIC BY R. HINDLEY
- Quicksort.
- Tiny C – sheer genius!
- Plan B
- C 89
- Mifid II
- Rust types. and Cyclone.
- Badly behaved polynomials.
Consequently, to overcome this restriction, the implementations of Rust’s standard libraries make widespread use of unsafe operations, such as “raw pointer” manipulations for which aliasing is not tracked. The developers of these libraries claim that their uses of unsafe code have been properly “encapsulated”, meaning that if programmers make use of the APIs exported by these libraries but otherwise avoid the use of unsafe operations themselves, then their programs should never exhibit any unsafe/undefined behaviors. In effect, these libraries extend the expressive power of Rust’s type system by loosening its ownership discipline on aliased mutable state in a modular, controlled fashion: Even though a shared reference of type &T may not be used to directly mutate the contents of the reference, it may nonetheless be used to indirectly mutate them by passing it to one of the observably “safe” (but internally unsafe) methods exported by the object’s API – from
Proposition: there are no major applications in any safe language that do not depend on either C libraries or “unsafe” magic keywords or both.