Lean and the upcoming Cyber Resilience Act

Stream: general

[Shreyas Srinivas]

I think this thread from the coq zulipchat on the EU's upcoming Cyber Resilience Act is relevant here: https://coq.zulipchat.com/#narrow/stream/237655-Miscellaneous/topic/Coq.20and.20Cyber.20Resilience.20Act/near/377765845

[Shreyas Srinivas]

In particular, the update from July

[Shreyas Srinivas]

Kevin Buzzard said:

I think that the observation that opening lean code can wipe your hard drive is in some sense far more concerning but this has been known for years and again it's never been an issue for me in practice -- I mark students' work in a virtual machine but this is not difficult to set up.

I was reminded about it when you mentioned this.

[Notification Bot]

3 messages were moved here from #general > PSA about trusting Lean proofs by Kyle Miller.

[Ioannis Konstantoulas]

The linked thread is so depressing :( I understand the need for software standards, but trapping open source like this is antithetical to fundamental liberties. I am very concerned about the proposed legislation, and more depressingly, don't see anything we can do to influence the results.

[Shreyas Srinivas]

Ioannis Konstantoulas said:

The linked thread is so depressing :( I understand the need for software standards, but trapping open source like this is antithetical to fundamental liberties. I am very concerned about the proposed legislation, and more depressingly, don't see anything we can do to influence the results.

The blogpost from Apache SF in that thread provides a good picture of the state of the legislative process. In that they explain that the MEPs explicitly want OSS to be included, because a lot of European businesses are SMEs and asking them to check their entire software stack (90-95% of it being OSS they use) is too expensive

[Shreyas Srinivas]

It is a very hard claim to make that Lean is purely academic when at least two of its creators (for Lean 4) are working in corporations. What seems relevant is whether people employed in some commercial capacity contribute to it (even if the project itself is run in an independent manner). The exceptions carved out for OSS are very very limited and might probably not cover Lean. Only lawyers can tell, and a lot depends on court precedents.

[Shreyas Srinivas]

What is less clear is what standards apply to ITPs. Because as the ASF post explains, the MEPs acknowledge that there are no standardised norms in many cases, and it seems that the community will have to come together and agree on what these standards will be.

[Shreyas Srinivas]

It would be nice to learn how Lean FRO will approach the requirements of the CRA.