| layout | title |
|---|---|
default |
Frequently asked questions |
Project Verona is a research project being run by Microsoft Research with academic collaborators at Imperial College London. We are exploring research around language and runtime design for safe scalable memory management and compartmentalisation. The prototype here only covers the memory management aspects of the research.
There are several areas we are investigating in Project Verona. A few of the high-level questions are here:
-
If we design a language without concurrent mutation, can we build scalable memory management?
-
Can linear regions be used to remove the restrictions of per-object linearity without sacrificing memory management?
-
Can language level regions be used to support compartmentalisations?
We are at different points in our research for these questions, and will submit academic articles for peer review in due course.
Project Verona is a research language that is inspired by ideas from other languages:
Many of the ideas we built on have been popularised by Rust, such as borrowing and linearity, and Pony, such as reference capabilities.
Backwards compatibility adds a lot of impedance and constraints on research. With Project Verona we have chosen to start with a clean slate to see what can be achieved towards our research questions. The ideas we develop hopefully can be tamed and fed back into existing languages in a backwards compatible way.
This is a research project not a product. Sometimes research projects turn into products, e.g. F#, but normally they do not! We hope the ideas we research can benefit other languages.
Project Verona is a research project that is not affecting engineering choices in the company.
The Project Verona team is connected to the people using all the major languages at the company, and want to learn from their experience, so we can research the problems that matter.
We are open sourcing at this stage to collaborate with academic partners on the language design. We want to conduct this research openly to benefit the community in general.
This is really two questions.
The runtime is inherently using a lot of unsafe code: it is producing the abstraction from the raw bits and bytes into the abstraction that the language uses. It is also inherently racy providing numerous lock-free datastructures for messaging and scheduling work. The runtime is also providing memory management concepts:
- the allocator, snmalloc, we designed for the runtime
- the management of regions of memory
- reference counting of various runtime concepts
- ...
Hence, the implementation requires very low-level access to the machine, that cannot be found in any safe language that we know of. When we started the project, C++ has the best tooling for handling unsafe code. Rust would be an interesting choice to understand what abstraction we could surface to Rust. As the concepts we are surfacing are different to Rust's type system it is unclear how beneficial this would be.
Ultimately, we want to verify the runtime against a formal specification, but this is a massive undertaking and is on the boundary of current verification research.
One of our core aims with Project Verona is to support high-quality C++ FFI. To support this, we will need extremely tight integration with a C++ compiler, like Clang. Using C++ as the implementation language of our compiler makes this integration much simpler.
Self-hosting the front-end of the compiler is a long-term possibility.