nostr:nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpqncxka2nmkqkndk4wkuf3tz3l39z9m8xax3aen3h8tvudwgjmf5mq4uv2v2 I haven't fully thought this through so maybe I'm wrong, but I feel like a _full_ corr...
@nprofile1q...
Often a bit simpler. The specification of a sorting algorithm, for example, may just be a post condition that, for all indexes n and n+1, the value at n+1 is greater than or equal to the value at index n. That’s simpler than, say, a quicksort implementation. But the proof that quicksort satisfies this specification is often more complex than the quicksort.
Often a bit simpler. The specification of a sorting algorithm, for example, may just be a post condition that, for all indexes n and n+1, the value at n+1 is greater than or equal to the value at index n. That’s simpler than, say, a quicksort implementation. But the proof that quicksort satisfies this specification is often more complex than the quicksort.
1
