4 ms·

> if the software you were running was advertised as formally verified as free of bugs. Nobody should be advertising that. Even ignoring the possibility of bug

> if the software you were running was advertised as formally verified as free of bugs. Nobody should be advertising that. Even ignoring the possibility of bugs in the runtime, there could also be bugs in the verifier and bugs or omissions in the specification. Formally verified never means guaranteed to be free of bugs.

gopiandcode 7mo ago
As quoted in the article itself, please take it up with the chief architect of the Lean FRO: > ... converted zlib (a C compression library) to Lean, passed the test suite, and then proved that the code is correct. > Not tested. Proved. For every possible input. lean-zip
- IshKebab 7mo ago
  Yeah well he shouldn't. That looks like slop tbf.