Archived tweet #9629 from the @leastfixedpoint Twitter Archive@DRMacIver @slava_pestov The similarity I see is that both get you up against the coal face: they both show "here is how things are *right now* - what should we do next?". Smalltalk does this by running the code. Coq, by imagining running the code. Uh, roughly.