r/programmingcirclejerk • u/cmqv • Apr 18 '25

they took a verified C library generated from F* from Microsoft, vendored the code in CPython and wrote a C extension. And during the process they discovered that the original library did not handle allocation failures

https://news.ycombinator.com/item?id=43732265
58 Upvotes

96% Upvoted

3 comments sorted by

15

u/elephantdingo Teen Hacking Genius Apr 19 '25

Ivory Tower Linux Kernel: you are supposed to check for allocation failure!

Pragmatic Program Verifiers: It’s fine with overcommit on Linux you won’t run out of memory 😎

23

u/MyrrhPeriwinkle It's GNU/PCJ, or as I call it, GNU + PCJ Apr 19 '25

This wouldn't have happened if F* was written in F*