To elaborate: you tell the computer a specification ("what to do"), you tell the computer an implementation ("how to do it"), and then you get the computer to check that the implementation conforms to the specification.