coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Safe to download and compile .v from evil source ?

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Timothy Carstens <intoverflow AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Safe to download and compile .v from evil source ?
Date: Sat, 1 Feb 2020 20:50:15 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f181.google.com
Ironport-phdr: 9a23:i+DQBR9S9xFld/9uRHKM819IXTAuvvDOBiVQ1KB31eMcTK2v8tzYMVDF4r011RmVBNmdt6kP0LWe8/i5HzBZutDZ6DFKWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3wOgVvO+v6BJPZgdip2OCu4Z3TZBhDiCagbb9oIxi6sArcutMZjIZsJao8xBnEqWZMd+hK2G9kP12ekwvy68uq4JJv7yFcsO89+sBdVqn3Y742RqFCAjQ8NGA16szrtR3dQgaK+3ARTGYYnAdWDgbc9B31UYv/vSX8tupmxSmVJtb2QqwuWTSj9KhkVhnlgzoaOjEj8WHXjstwjL9HoB+kuhdyzZLYbJ2TOfFjeK7WYNEUSndbXstJWSJPAp2yYZYMAeUDM+ZWqIbyqEcBoxalGQmhBvnixiNSi3Pqw6E31fkqHwHc3AwnGtIDqHrYrNfyNKcUUOC1z7fHzTHdYPxIwjr9543IfQogofGIR75/bc3RyUwhGwjYiViQq4vlPzWU1uQOrWeb6/RvWvy0hm4orgF+uDmvxsM2hobVgYIVz0nJ+CNky4g2Pd21UFB3bcKgHZdKtCyXN5F6Tt4jTm10oio2174LtYOjcCQUyZkr2wPTZvmaf4WM/h3uUemcLDZkiH55fb+zmhW//Eqlx+LhS8a50lhHoy9Hn9TNrH8A1Rne5dKHR/Z//kqs3DWC2x3J5exGJ00/iLDVJIQ7wrEqk5oeqUTDETHymEXxlKKWc18r+ums6+j+e7XmuoKQO5Z6ig3jMakih9azAes/MggJUGib/fqz2Kf/8k3+RbVGlvw2kq/Hv5DGPckXuLK1DgtP3osg6xuzFSqq3dUEkXUdMV5Iew+Lg5DsO17UIfD4Cfm/g06rkDdu3/3GPLrhApPMLnjAjrjheahy5FBHxQo8yNBQ/ZNUCrUbLP3vXU/xscTUDgUlPAys3+bnFNJ925sCVmKIG6+VKb/dsVuV5u00OOSMf48UuDPlK/c//fLujHk5mUUcfaazx5cXZmq4TbxaJBClYH/rntcQWUwDpBEiQerxwAmDVyJUeXuoUaY7+Rk0DYunCcHIQYX705Kb2yLuVJ9RYGFFB1SBHF/ncoyFX7EHbyfYaptjlToFVrWlRoIJ2hSntQu8wL1ieLmHshYEvI7ugYAmr9bYkgs/oGQtXpatllqVRmQxpVsmAjo/3aRxu0t4kw7R3q1xgvgeHttWtaoQD1UKcKXExuk/MOjcHwLMetDTFgSjS9SiRCgtF5c/mo9XJUl6HNqmg1bI2C/4W+ZJxYzOP4Q99+fn51a0P9x0ki+U26wojl1gScxKZzWr

On Sat, 1 Feb 2020 15:35:53 -0800
Timothy Carstens
<intoverflow AT gmail.com>
wrote:

> ...
> For this reason, containers & VMs are awesome for sharing working
> environments, but are expensive and error-prone as a security
> boundary. Best practice yes, but only as a last line of defense.

Containers & VMs are a line of defense one should always have, whether
it is first line or last line doesn't change the expense and complexity.

Sure I'd prefer the Coq environment to have a small attack surface and
well defined requirements. But I'm still going to use a container
regardless. So the expense and complexity of the container is always
felt.

Are you suggesting instead that you'd prefer the Coq environment be
made so that containers are unnecessary?

[Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/01/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Jay Kruer, 02/01/2020
  - Re: [Coq-Club] Safe to download and compile .v from evil source ?, Andres Erbsen, 02/01/2020
    - Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/01/2020
    - Re: [Coq-Club] Safe to download and compile .v from evil source ?, Tej Chajed, 02/01/2020
      - Re: [Coq-Club] Safe to download and compile .v from evil source ?, jonikelee AT gmail.com, 02/02/2020
      - Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/02/2020
      - Re: [Coq-Club] Safe to download and compile .v from evil source ?, Clément Pit-Claudel, 02/02/2020
        
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/02/2020
        
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, jonikelee AT gmail.com, 02/02/2020
        
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/02/2020
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, Marco Servetto, 02/02/2020
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, Jason Gross, 02/02/2020
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/02/2020
        
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, jonikelee AT gmail.com, 02/02/2020
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/02/2020
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, Jason Gross, 02/02/2020
        
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, jonikelee AT gmail.com, 02/02/2020
        
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, Adam Chlipala, 02/02/2020
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, Théo Zimmermann, 02/02/2020