[HN Gopher] Re-fixing Servo's event-loop
___________________________________________________________________
Re-fixing Servo's event-loop
Author : Ygg2
Score : 93 points
Date : 2024-08-14 13:36 UTC (9 hours ago)
(HTM) web link (medium.com)
(TXT) w3m dump (medium.com)
| baq wrote:
| Didn't expect to find a TLA spec here! Criminally underused tool
| in our industry.
| nextaccountic wrote:
| 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
| JasonSage wrote:
| 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.
| bsaul wrote:
| I'm so glad the industry starts adopting formal proofs more and
| more... After 20 years in the industry i still feel like a
| caveman, coding as best as i can, hoping nothing bad will happen
| (and then sighing at the sight of the 100ks line counts of my
| project).
|
| Maybe having more powerful code generators like LLMs will shift
| us toward spending more time on specification and modelling ?
| Let's hope so.
| diggan wrote:
| 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 ;)
| bsaul wrote:
| 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.
| sanxiyn wrote:
| Try property testing. Property tests written by myself
| routinely discover bugs in my codes.
| Aerbil313 wrote:
| Contrary opinion: Writing your program is much easier once
| you write the proof, because you basically formulate your
| entire program.
| wongarsu wrote:
| 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.
| aumerle wrote:
| The end of the article says the bug isn't fixed, so presumably,
| the root cause identification was wrong?
| proneb1rd wrote:
| This is how medium blogs look like. I can't believe people still
| post there https://imgur.com/a/2PpS14h
| touwer wrote:
| Imgur is not much better ;)
___________________________________________________________________
(page generated 2024-08-14 23:01 UTC)