linebender

Formal Web: a modular Web engine written in Rust and using formal methods Reposting; this time with a focus on why it is not a code dump. The project I would like present is a web engine written in Rust. It does not break new grounds in the sense of being the first Web engine in Rust, because we have had a Web engine for a long time, where I am myself involved as a maintainer and Technical Steering Committee member: Servo. However, this is not a code dump either, because: - Myself, and others, have been working on this since March of this year. - This post is a "full fledged post", which is supported by a linked-to longer essay (see below) - I will below explain the relevance for the Rust community - I will compare it with other Web engines written in Rust. ---- Ok so now that this is out of the way, here is the actual post: gterzian/formal-web is a new prototype of a Web engine written in Rust. It is relevant for the Rust community, because it provides us with something new: - a multi-process graphics stack based on modern Rust components, like Vello and Wgpu, paired with a modular design allowing deeper platform integration, for example integrating with Core Animation and using IOSurface on Apple platforms. - A modular approach to integrating a Javascript engine, so that you can "bring your own engine". Currently V8 and the all Rust Boa are supported out of the box, and other engines, Like the also all Rust Nova, could be integrated through the implementation of various traits. - Use of Blitz components, blitz-dom and blitz-paint, as a kind of DOM engine inside the Web engine. - Use of formal methods to model check multi-process Rust code, based on the approach described at Validating Traces of Distributed Programs Against TLA+ Specifications - Modularity of various other layers, such as: networking, media, and the starting of and communication with process-like sub-components. - An embedder API that makes it easy to do various platform specific integrations, such as using a display link on Mac. - An explicit goal of eventually being able to Ship on IOS in the EU as per Apple's guidelines. How is this different from other Web engines in the Rust ecosystem? Difference with Servo: the graphics stack of Servo does not isolate GPU operations in a dedicated process and it is based on an OpenGL stack. Difference with Blitz: while Blitz does integrate well with Vello/Wgpu, it is not designed around process isolation of either GPU operations or the running of Javascript, making it less suitable for the Web use-case where you essentially run untrusted code downloaded over the internet. While it does use Anyrender as modular render target, it does not offer modularity at the lower-level end of the graphics pipeline. Neither engines allow swapping out JS engines, and neither allow for deep platform graphics integration like Core Animation based compositing on Mac (which can make a large difference in terms of battery life). For a walk-through of the entire flow involved in rendering a frame of Web content, see the introduction essay: How I am building a Web engine. The essay also contains a gif showing the benefits of Core Animation on Mac, where only relevant parts of the screen are re-rendered. Please let me know what you think. I can also use help implementing countless Web standards.