alt Hacker NewsCurious question, in this case for verification they ported the software into a formal mathematical model. Why can't software development start from the other end instead ? Start with a formal model with the properties you want, then translate it into software.
You can. It ends up really slow normally which is why we don't do it. For example for a proven Deflate, it took an hour to process a 1MB file https://ar5iv.labs.arxiv.org/html/1609.01220