I think the first paragraph (with the exception of the NP time sentence) is a good description of what I would call a “nondeterministic program” (or “nondeterministic procedure”, etc). And I think the page does confuse the connection between nondeterministic programs and algorithms expressible on nondeterministic platforms (like NFAs and nondeterministic Turing machines), which is what NP time is about.

Something that I’ve seen frequently in the literature and in conversations here is that contracts and types are very different. I‘m having trouble understanding this, since contracts look a lot like a type system that works at run time.

I’ve also seen the idea that types and contracts can be complementary, but I’ve really only seen languages use one or the other. And, in the case of Typed Racket, it appears that contracts are simply used like dynamic versions of the static types.

What’s the fundamental difference between types and contracts? And, if possible, what’s an example of them being used together (outside of Typed Racket)?

The data/enumerate library uses contracts to run first-order checks on enumerations that generate inputs and verify they uphold the invariants expected of enumerations

After revisiting the paper, Oh Lord, Don’t Let Contracts Be Misunderstood, I think that a simple explanation is, types enforce the structural consistency of programs, whereas contracts enforce the satisfaction of detailed invariants.