alt Hacker NewsThere's a lot of claim and so little technical details on that page.
How was the formalization of Python accomplished? What formal proof framework do you use?
How do you reproduce the optimizations across several instances / runs of the program? (since the source code doesn't change... assuming you don't redo the same work over and over?)
What visibility, tracking and logging is there into the actual code running? Debugging is an extremely important part of building software, especially if there's a demon switching out binary code constantly underneath. Even if the recompiler is perfect (it won't be), user code never is.
Why is the superoptimization and visibility into the data not surfaced back to the level of the source code? This seems like a waste.
More technical details forthcoming of course, including about formalisation... We indeed do not redo the same work over and over, but rather cache intelligently. We take special care not to interfere with debugging workflows (much in the same way that, e.g., the Tier 2 JIT does, in CPython). And as for visibility into the level of source code, what do you mean? The rewritten binary portions don't always have associated code, let alone in the language of origin.