giltho

Fantastic work

Beyond academic research, a non-exhaustive list of people using either Lean or related tech:

- Amazon (where they even hired the creator of Lean to pursue this)

- Microsoft (mostly cryptography but also other stuff) - ARM (hardware verification)

- Apple (hardware verification, that I'm aware of)

- Lots of companies verifying things for blockchain technologies if you're into that

- More specialised companies, e.g. Galois Inc.

Hey chatGPT, summarise this post for me

Imagine 50 years of computer security to have articles come up on hackernews saying “what you need is to allow a black box to run arbitrary python code” :(

A common specification language is a very ongoing discussion, we just haven't managed to find an agreement yet.

Things like `#[no_panic]` make sense, but it also doesn't require a spec language at all, the compiler already has support for these kinds of annotation and anyone could catch it. Though I cannot think of a single verification use case where all I want to check is the absence of panic.

I can assure you that the person who wrote this is very well aware of the subtleties involved with formalising the law. Law + Programming is an active research field (https://popl23.sigplan.org/home/prolala-2023), and it is very far away from anything like smart contracts, it is full of brilliant people who have no pretension of replacing the law with computers, but simply be helpers where they can.