A nice intro/showcase to Coq, I suppose. But the triviality of this frankly makes it difficult for me to understand what value this has and what it teaches us - we've just proven that one kind of syntax is equivalent to…
In 2022, "state of the art" is throwing a deep net at it. It will likely pick up on all of these findings (and better ones, incomprehensible to us) by itself given correct architecture and enough data, but I can't help…
Any reason they aren't using formal verification for this kind of thing? It would seem like a very worthy investment.
The Bible of formal software logic, free of charge: https://softwarefoundations.cis.upenn.edu/
A nice intro/showcase to Coq, I suppose. But the triviality of this frankly makes it difficult for me to understand what value this has and what it teaches us - we've just proven that one kind of syntax is equivalent to…
In 2022, "state of the art" is throwing a deep net at it. It will likely pick up on all of these findings (and better ones, incomprehensible to us) by itself given correct architecture and enough data, but I can't help…
Any reason they aren't using formal verification for this kind of thing? It would seem like a very worthy investment.
The Bible of formal software logic, free of charge: https://softwarefoundations.cis.upenn.edu/