Remix.run Logo
NewsaHackO 3 hours ago

To me, saying that there is a bug in the lean runtime means lean-zip has a bug is like saying a bug in JRE means a Java app that uses the runtime has a bug, even though the Java app code itself does have a bug. It seems like the author is being intentionally misleading about his findings.

brabel 26 minutes ago | parent | next [-]

No. It would be like finding a memory unsafe caused bug in a Java application that is due to a bug in the JRE. That would absolutely warrant a title like “I found memory unsafe bug in my Java code” when everyone expects Java code to be memory safe, which is analogous to the article in question.

aidenn0 3 hours ago | parent | prev [-]

I think it's ambiguous and fair game for the idea of answering the question "if we write programs in this manner, will there be exploitable bugs?