Re-fixing Servo's event-loop(medium.com)
medium.com
Re-fixing Servo's event-loop
https://medium.com/@polyglot_factotum/re-fixing-servos-event-loop-e00bdf267385
28 comments
In the last decade or so there has been an explosion in the popularity of explicitly typed languages. Typescript, typed python, Rust with its very strict and expressive type system, etc. That's not full formal proofs of the entire behavior, but it's a solid step back in that direction.
Imho any change in this direction is predicated on tooling and developer experience. Explicit typing was made easier by smarter autocomplete from better IDE plugins, and those same plugins make more valuable suggestions if you have better types, creating a virtuous circle.
Nothing of the form exists so far for formal proofs. If you limit it to small sections of behavior it might pass as a smart but obscure way to write unit tests (ensuring that certain behaviors hold). But nothing outside of your unit tests benefits from it.
Maybe making the specification the starting point from which an LLM writes code changes that. But so far all the evidence points to people being very bad at writing specifications and preferring imperative over declarative languages.
Imho any change in this direction is predicated on tooling and developer experience. Explicit typing was made easier by smarter autocomplete from better IDE plugins, and those same plugins make more valuable suggestions if you have better types, creating a virtuous circle.
Nothing of the form exists so far for formal proofs. If you limit it to small sections of behavior it might pass as a smart but obscure way to write unit tests (ensuring that certain behaviors hold). But nothing outside of your unit tests benefits from it.
Maybe making the specification the starting point from which an LLM writes code changes that. But so far all the evidence points to people being very bad at writing specifications and preferring imperative over declarative languages.
> Rust with its very strict and expressive type system
Tangentially, I find it very interesting how Rust could have had fully inferred types (like OCaml does), but chose to require specifying types at function boundaries.
It shows a thoughtful balance of what the system can technically do, and what's actually useful to the humans dealing with the code.
Tangentially, I find it very interesting how Rust could have had fully inferred types (like OCaml does), but chose to require specifying types at function boundaries.
It shows a thoughtful balance of what the system can technically do, and what's actually useful to the humans dealing with the code.
Rust doesn’t have a very expressive type system. Rust type system would have been at home twenty years ago. Ocaml already had a better type system when I used it professionally in the 2010s and they have added a lot since and you could already type infer everything.
I’m sorry but implying that having typing becoming a bit more popular is a significant step towards formal proof is akin to saying we are getting closer to using efficient heating because we have switched from burning peat to coal.
I’m sorry but implying that having typing becoming a bit more popular is a significant step towards formal proof is akin to saying we are getting closer to using efficient heating because we have switched from burning peat to coal.
If more languages adopted Design by Contract, and the capabilities for Type Driven Development, we would already be much better, without formal methods, many of which aren't supported in common languages and there is always something lost in translation.
> there is always something lost in translation.
SPARK is more than 20 years old at that point and allows you to easily use formally proven code next to other ADA code. Sorry but implying that the issue is things “lost in translation” is a complete cope out.
I’m very sour about the disdain for formal proof in the field. I understand the wish to iterate fast for user-facing elements but the fact that we use the same development techniques for the backbone of our infrastructure is nothing short of insane from my point of view.
There is a self defeating attitude with regard to formal tool which is that they are too costly and too complicated to use outside of things for which they are mandatory. It means people are not trained in how to use them so it’s hard and costly to find someone who will prove your code and this vicious cycle somehow feeds itself.
SPARK is more than 20 years old at that point and allows you to easily use formally proven code next to other ADA code. Sorry but implying that the issue is things “lost in translation” is a complete cope out.
I’m very sour about the disdain for formal proof in the field. I understand the wish to iterate fast for user-facing elements but the fact that we use the same development techniques for the backbone of our infrastructure is nothing short of insane from my point of view.
There is a self defeating attitude with regard to formal tool which is that they are too costly and too complicated to use outside of things for which they are mandatory. It means people are not trained in how to use them so it’s hard and costly to find someone who will prove your code and this vicious cycle somehow feeds itself.
My "lost in translation" remark naturally doesn't apply to SPARK, rather to stuff like TLA+ that don't have any mapping to actual programming languages, unlike stuff like Ada/Spark, Frama-C or even Design by Contract.
It is meaningless to model a great algorithm in abstract mathematical models, and then let someone else implementing them in C89 with raw BSD sockets and C strings, without any relation between the mathematical model and the C implementation.
It is meaningless to model a great algorithm in abstract mathematical models, and then let someone else implementing them in C89 with raw BSD sockets and C strings, without any relation between the mathematical model and the C implementation.
>It is meaningless to model a great algorithm in abstract mathematical models, and then let someone else implementing them in C89 with raw BSD sockets and C strings
Bold statement, at least in that case you know the algorithm isn't wrong.
Bold statement, at least in that case you know the algorithm isn't wrong.
Which is worthless without the guarantee that the C code actually implements the algorithm as designed.
Something that manual translation cannot provide.
If the algorithm was validated in F*, and having the C code generated, great.
Now doing it in TLA+, and then implementing it as copying from a algorithms and datastructures book with Pascal like pseudo-code, not so great.
Something that manual translation cannot provide.
If the algorithm was validated in F*, and having the C code generated, great.
Now doing it in TLA+, and then implementing it as copying from a algorithms and datastructures book with Pascal like pseudo-code, not so great.
You are right that it would be great if the code was generated automatically, but wrong that there is no value in using TLA otherwise.
When you are writing code, do you have an idea in your mind of what you are trying to implement? TLA is not for checking the code, it is for checking that idea. I explain this in more details in another article: https://medium.com/@polyglot_factotum/why-tla-is-important-f...
When you are writing code, do you have an idea in your mind of what you are trying to implement? TLA is not for checking the code, it is for checking that idea. I explain this in more details in another article: https://medium.com/@polyglot_factotum/why-tla-is-important-f...
Some (balanced) automated testing gets you away from "hoping nothing bad will happen" while not having to spend a year coming up with a formal proof for your program. Worth testing if you haven't ;)
of course, i do test. But let's be honest, if the person writing the tests is the same as the one writing the code, chances are the tests won't discover flaws in the model of the original design.
I think there's definitely something to the notion that there will be correlation between things you forget to (try to) guarantee in your code and things you think to test for. It's not clear to me that it's meaningfully stronger than the correlation with things you forget to prove.
Any which way, more prodding of the model (mental or more formal) is probably going to help correctness but may or may not be worth the cost, depending.
Any which way, more prodding of the model (mental or more formal) is probably going to help correctness but may or may not be worth the cost, depending.
Try property testing. Property tests written by myself routinely discover bugs in my codes.
Contrary opinion: Writing your program is much easier once you write the proof, because you basically formulate your entire program.
The end of the article says the bug isn't fixed, so presumably, the root cause identification was wrong?
Didn't expect to find a TLA spec here! Criminally underused tool in our industry.
There's a model checker that can directly verify Rust code, Kani https://model-checking.github.io/kani/ - I wonder if Servo could use it in this case?
Or maybe https://github.com/tokio-rs/loom
Or maybe https://github.com/tokio-rs/loom
The problem with most of these tools is the same as when we got the UML driven development craziness, most of them don't map to the actuall source code being written, and most often than not, mistakes get introduced as the actual implementation doesn't match the model.
What the industry is missing is more adoption of Design by Contract, formal verification clauses (SPARK and Frama-C style), Type Driven Development, across mainstream languages, alongside more love for stuff like Dafny, F* and such.
What the industry is missing is more adoption of Design by Contract, formal verification clauses (SPARK and Frama-C style), Type Driven Development, across mainstream languages, alongside more love for stuff like Dafny, F* and such.
If you haven't seen those already, you might also want to check out:
- Apalache: a symbolic model checker for TLA+ backed by Z3 (https://apalache-mc.org)
- Quint: a modern and executable specification language with TLA+-like semantics, that integrates with Apalache (https://quint-lang.org)Quint looks great, thanks for the link!
I also didn't expect to find it, partially because I've had basically no exposure to it... I've heard about these formal verification tools but I never really grasped them or felt like they applied to any of the problem domains I work in.
But WOW did the example here really drove home how it could be a very useful tool for me. I can think of a few projects I've worked on or reviewed in the last year where I'd have considered using this, and still am.
But WOW did the example here really drove home how it could be a very useful tool for me. I can think of a few projects I've worked on or reviewed in the last year where I'd have considered using this, and still am.
This is how medium blogs look like. I can’t believe people still post there https://imgur.com/a/2PpS14h
I think medium still does a lot of really good SEO for free. My last company moved from self-hosting to medium because the same content on medium drove more views and generated more leads.
But this was a few years ago, so maybe this effect has since collapsed on itself.
But this was a few years ago, so maybe this effect has since collapsed on itself.
[deleted]
Maybe having more powerful code generators like LLMs will shift us toward spending more time on specification and modelling ? Let's hope so.