homodeus

4 ms·

1. 1.▲
   by homodeus 4y ago

   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 another, b
2. 2.▲
   by homodeus 4y ago

   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 but fe
3. 3.▲
   by homodeus 4y ago

   Any reason they aren't using formal verification for this kind of thing? It would seem like a very worthy investment.
4. 4.▲
   by homodeus 4y ago

   The Bible of formal software logic, free of charge: https://softwarefoundations.cis.upenn.edu/