From: janburse@fastmail.fm   
      
   In halls of Cambridge, where catnip sways,   
   Sat pioneers lost in existential haze.   
   “Here lies a term!” they cried, “both bound and free,   
   A bag of possibilities, as far as we see.”   
      
   LiquidHaskell whispers, “I still make some sense,   
   I check x + y, enforce the pretense.   
   But only 1% — the rest, pure ado,   
   Existentials and predicates, I haven’t a clue.”   
      
   Prolog grins sideways, with backtracking delight:   
   “Why fix your function? Let each path take flight!   
   X and Y and Z — all three may roam,   
   I’ll find a solution, or many, for home.”   
      
   Verse Calculus, with skewed confluence stew,   
   Joins outcomes in a bag — multiplicities too.   
   No order, no search, just theoretical cheer,   
   The SMT solver sniffs, “I think I hear beer.”   
      
   Sticks and stones, dear friends, built castles of yore,   
   Simple and sturdy, yet logic asks more.   
   Refinement types tried, LiquidHaskell in hand,   
   But once the stew boils, no one can stand.   
      
   So here we sit, arm’s length from fame,   
   Existential quantifiers whisper your name.   
   A mockery? Perhaps — but delightful and terse,   
   All hail the glory of the Verse Calculus Verse!   
      
   Franz Sneijders schrieb:   
   > Mild Shock wrote:   
   >   
   >> We use “∃” to bring a fresh logical variable into scope, because we   
   >> really mean “there exists an x such that ···.”   
   >   
   > idiot, there is no any x over there. And it doesn't need to be a variable,   
   > a constant suffices.   
   >   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)