undefined | Better HN

0 pointsIshKebab2mo ago0 comments

> 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.

0 comments

2 comments · 1 top-level

gopiandcode2mo ago· 1 in thread

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

IshKebabOP2mo ago

Yeah well he shouldn't. That looks like slop tbf.

j / k navigate · click thread line to collapse