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.
> single verification use case where all I want to check is the absence of panic.
Basically any decoder/deserializer. It might be sufficient to handle the correctness in tests but panics are the most severe thing you want to avoid.
How well `#[no_panic]` actually works in practice?
There might be cases where e.g. index access violation never happen but compiler might still think that it happes. I could be impossible to restructure code without adding some performance overhead.
#[no_panic] has false-positives, but no false-negatives. If it’s present, the code won’t panic and can’t panic.
Index access violation that “never happens” is the root of every buffer overflow, so I’m absolutely OK with the minimal overhead behind the bounds check for actual safety
> Though I cannot think of a single verification use case where all I want to check is the absence of panic.
Not for verification but in terms of ease of use, having no panic in a program means it would be fine and safe to have pointers to uninitialized memory (it's currently not because panics means your destructors can be run anywhere in the code, so everything must be initialized at all time in safe rust).
One more case where the halting problem adds more confusion than it helps. The halting problem is equivalent to the acceptance problem, which is equivalent to the reachability problem.
>Though I cannot think of a single verification use case where all I want to check is the absence of panic.
You can reduce any static verification task to a check for a condition that produces a panic. In short, sprinkle your pre, post and intermediate conditions all over your code in a way that produces a panic (known as asserts) and the tool will do the heavy lifting.
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.
Sure, I think I posted my response not because "it could never solve ANY problems," but instead "way too many non-lawyers, especially techy-non-lawyers, have the deeply misplaced idea that is a very important, perhaps THE most important, problem to solve in the law." It's just not very high on the list at all.
Maybe not for lawyers, no. But as a citizen I'm expected to comply with the law, with many many laws. It'd actually be nice if law was slightly more formally verifiable, so it would be easier for me to understand what to comply with.
Being able to break down clauses into more logical normal forms would probably greatly enhance the possibility of compliance.
For every bit of gained clarity, you'd also gain a ton of people like the "sovereign whatever" idiots who just love trolling, with the added negative of them having more "formal proof" of their untenable silliness.
