2 ms·

Proving that your algorithmic design is correct (to the degree the proof tool can assure) is already a big help - even if your implementation of the algorithm m

Proving that your algorithmic design is correct (to the degree the proof tool can assure) is already a big help - even if your implementation of the algorithm might still have bugs. At least now you know it's just bugs you need to fix, and not a faulty logic to begin with.

pjmlp 2y ago
Faulty logic can only be proven to a specific mathematical limit, if the actual system constraints, hardware and OS APIs, aren't part of the model.
- coldtea 2y ago
  My comment was already about proofs "to a specific mathematical limit" still being useful and better than nothing, tho