The Coq mailing list

[Andreas Bogk <andreas AT andreas.org>]

Excerpts from guninski's message of Mi Mai 04 13:50:13 +0200 2011:
>   Proof.
>     external "/bin/sh" "ESCAPE_SEQ; write_vo_proof; nicely_kill_coq ;" True.
>     (* this invokes /bin/sh. suited for formal software verification *)
>   Qed.

FWIW, I think that this "external" feature, as well as the loading of 
arbitrary
plugins, are indeed a problem.  Coq is more and more being used for software
engineering for critical systems.  There's a huge benefit in being able to
specify desired behaviour of subsystems formally, and have the author of the
subsystem prove that his implementation fulfills the specification.  The 
ability
to break proof checking by the tricks demonstrated mean we're back at having 
to
read every single line of code of the subsystem, instead of being able to just
read the specification and leave the details to the proof checking engine.

My suggestion would be:

 * Remove the "external" feature, or make it optional, with "turned off" being
   the default
 * Split load paths for .vo files and coq plugins, make plugin load path
   default to system directories only, inhibit manipulation of plugin
   load path from within .v files.

Regards,
Andreas

P.S.: I also suggest stopping remarks about hacker reputation. Georgi already
maxes out any scale.