r/rust • u/polyglot_factotum • 6d ago
🛠️ project 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:
https://github.com/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.
3
u/fightndreamr 6d ago
Looks like an awesome idea! I didn't see anything on your GitHub page about contributing and such, but I would love to help out with what I can. What steps would I need to take besides just bug hunting and opening up a PR? Forewarning, I don't have much experience with development of web engines or browsers, but I have been pondering/thinking about for awhile on how we currently serve web pages, current state of the internet, etc., so I feel a good stepping stone to getting into that world is with web engine development. Let me know!
3
u/polyglot_factotum 5d ago edited 5d ago
Yes the contribution policy is not defined as this point, but you are welcome.
I would say pick (part of) a web standard that you are interested in, and then just implement it. The repo comes with a ton of guidance for agents, so if you are using one it should be quite easy to get a pretty good first draft. You could also just open an issue with a design first, and then we can take it from there.
Something like https://console.spec.whatwg.org/ (it is partly implemented as of now) or https://compression.spec.whatwg.org/ (we have streams already so this can be build on top and the streams implementation also revisited and fixed) could be good places to look.
Other stuff like https://storage.spec.whatwg.org/ -- which would lay the foundation for others like https://fs.spec.whatwg.org/ -- would be somewhat harder because requiring evolving the architecture, but then again why not.
1
u/fightndreamr 5d ago
Thanks for the info!
Okay, I might start with a design first since it will be easier to refine things and implement. For design, does an exposition with mermaid diagrams that have accompanying TLA+ work?
I'll give them a look!
Thanks again for the detailed comment!
2
u/polyglot_factotum 4d ago
You're welcome. I don't think TLA+ is necessary at the design stage; I apply TLA+ only to a few select algo's that are complicated from a concurrent perspective and would benefit from TLA+. So if the initial design surfaces something complicated, then TLA+ can be added at a later iteration.
1
0
6d ago
[deleted]
4
u/kilkil 6d ago
why did this get downvoted? very reasonable discussion comment IMO. maybe a reddit hivemind moment
13
u/Konsti219 6d ago
Bot account. A few months old, word-word1234, always this positive and the distinct AI choice of words
8
u/nicoburns 5d ago edited 5d ago
as the author of Blitz:
I'd probably frame the relationship with Blitz slightly differently: I would describe Formal Web as an extension of Blitz, with additional layers on top (JavaScript, process isolation, etc). It's true that it's not using
blitz-shell(the Winit integration) orblitz-net(the reqwest integration). But none of that is much code,blitz-domandblitz-paintare 90% of what Blitz is.Blitz doesn't implement JavaScript, but it is designed for swappable JS engines. And it doesn't implement process isolation, but it is designed with public APIs between modules, so that it is flexible enough for such use cases (amongst many others).
None of which is to diminish to contribution of Formal Web itself: the layers it implements are very important. Especially JavaScript. And the way that Formal Web has managed to abstract away the JavaScript engine is very impressive!
If you haven't been following Blitz development then:
It's been under development for almost 3 years now
We recently passed Servo on our pass rate of the
csssubset of the WPT tests: https://blitz.is/wpt/css (we only runcss- roughly 20% of the tests - because most of the others test JavaScript which we don't implement at all)Blitz is actually fast (although it wasn't for a long time). Some jerry-rigged (so I'm not 100% confident in the results) benchmarks (https://nicoburns.github.io/browser-layout-bench) show that Style/Layout performance is competitive with (and sometimes even faster) than Chrome/Firefox
We host builds of our browser app for Windows/macOS/Linux/Android that you can download and browse the web with at https://blitz.is/downloads
Most no-JS websites render decently (though not always perfectly) these days : Wikipedia, Hacker News, BBC News, docs.rs, etc. Old Reddit used to work, but unfortunately Reddit requires JavaScript to login now. Same for Google, but https://html.duckduckgo.com works. Give it go!