[TYPES/announce] Two phase reviewing for POPL; a response

[Adam Chlipala]

Alessio Guglielmi wrote:
> However, its results would clash dramatically with my expectations,
> and indeed those of my community. This is one of those cases where
> one says `it cannot be true'. The only way to judge is to check the
> details, and this takes days or weeks of study because there's some
> serious mathematics behind.
>    

This is one area where we can benefit from the shift towards 
machine-checked proofs that is already going on in this community.  If 
the theorem were proved with a proof assistant, then one would only need 
to audit the theorem statement and the definitions it depends on.  (Of 
course, understanding the structure of the argument would still be 
important, but not _as_ important.)

It would take a significant culture change to reach the point where a 
proof isn't believed if it isn't machine-checked, but I wouldn't want to 
bet against the POPL community reaching that point in the next few 
decades.  Because of that possibility, this particular reason in support 
of high time investment by reviewers may not need to be considered as 
fundamental.