alt Hacker NewsWouldn't it be more productive spending the tokens on adding ACSL annotations to verify CPython with Frama-C? You'd verify the actual runtime instead of an AI translation of it, and fixes could be contributed upstream directly.
Wouldn't it be more productive spending the tokens on adding ACSL annotations to verify CPython with Frama-C? You'd verify the actual runtime instead of an AI translation of it, and fixes could be contributed upstream directly.
One advantage of this approach is that it can be done both on the C implementation code and the Python standard library. It's a bit approximate -- automatic retrofitting of formal specification maybe it helps to think of it as a stepping stone for simple automated testing and property based testing.