| 21:38 | <Michael Ficarra> | at the TG5 call this morning, some EPFL researchers presented their work mechanising the RegExp section of the spec: https://github.com/epfl-systemf/Warblre |
| 21:39 | <Michael Ficarra> | they did this to show equivalence to their linear matching algorithm |
| 21:40 | <Michael Ficarra> | and at the same time proved that our spec doesn't have any assertion failures or out-of-bound accesses in that section (🎉) |
| 21:41 | <Michael Ficarra> | I was thinking we should invite them to an editor call to see if we could use the mechanisation to help us make refactorings, proving that they are semantics-preserving |
| 21:41 | <Michael Ficarra> | but first we should probably think what kind of refactoring we'd like to make to that section |
| 21:42 | <Michael Ficarra> | I know we're unhappy with it (especially @bakkot), but I don't know if there's any concrete plans for what we'd want |
| 21:43 | <Michael Ficarra> | another idea is that we could take the linear matching algorithm and derive the spec factoring from that (given we know it's semantically identical) |
| 21:45 | <bakkot> | my current unhappiness with the section is about the observable complexity, not the editorial specification |
| 21:45 | <bakkot> | we dealt with most of the glaring editorial issues |
| 21:46 | <Michael Ficarra> | it's still definitely weird |
| 21:46 | <Michael Ficarra> | like these are weird https://tc39.es/ecma262/multipage/text-processing.html#sec-countleftcapturingparenswithin |
| 21:48 | <Michael Ficarra> | also, they skipped Annex B and based their work on ES2024, but I don't think either of those is significant for this work |