The Coq mailing list

[David Leduc <david.leduc6 AT googlemail.com>]

BULLETIN - EAS ACTIVATION REQUESTED

TROLL WARNING
INTERNET COMMUNITY
RELAYED BY COQ-CLUB
DECEMBER 2 2011

THE FOLLOWING MESSAGE IS TRANSMITTED AT THE REQUEST OF THE COQ-CLUB COMMUNITY.

A CPDT TROLL WARNING HAS BEEN ISSUED FOR THE COQ-CLUB UNTIL FURTHER
NOTICE. ONE INTERNET USERS HAVE BEEN REPORTED POSTING ITEMS ON THE
COQ-CLUB TO ILLICIT A RESPONSE FROM OTHER USERS. THESE USERS ARE
CALLED TROLLS... AND WILL ONLY LEAVE IF YOU STOP RESPONDING TO THEM.
DELETING THEIR CONTENT HELPS TO FIGHT AGAINST TROLLS. DO NOT CALL
TROLLS NAMES. THIS
INCLUDES CALLING TROLLS TROLLS. CALLING TROLLS NAMES IS PART OF THE
EMOTIONAL RESPONSE THEY DESIRE. GIVING WARNING STATEMENTS WHICH PURELY
INVOLVE FUTURE ACTIONS IS NOT PART OF THE RESPONSE THEY DESIRE. IF
TROLLS CONTINUE TO PESTER YOU OR YOUR WEBSITE... DELETE THEM FROM
FRIEND LISTS... BLOCK THEM FROM WIKIS... AND/OR TAKE OTHER MEASURES TO
PREVENT THEM FROM TROLLING. TROLLING A TROLL WILL NOT HELP ELIMINATE
THE TROLL. TO REPEAT... DO NOT RESPOND TO TROLLS. DOING SO IS CALLED
FEEDING THE TROLLS... AND WORSENS THE PROBLEM.

On Tue, Nov 29, 2011 at 3:45 PM, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:
> I've resisted jumping in until now, but I think it's worth pointing out that
> some of us are very skeptical that declarative proofs are a good idea.  The
> style of imperative Coq proof that you see in the wild is not the only other
> option.  My book CPDT presents another style which I believe dominates both
> the common Ltac style and the declarative style (in any proof assistant) for
> ease of writing, reading, and maintaining proofs:
>   http://adam.chlipala.net/cpdt/
>