3 ms·

One of my favorite quotes on this topic is: "Type systems are just the parts of formal verification we've figured out how to make fast."

• honr 2mo ago
  Thankfully this is no longer strictly true. So, I think the quote needs a slight adjustment, "Type systems and $THING are just ...", but $THING is not very well defined yet. Between "linters", and other relatively fast AST-based rule enforcers, some of which looking at higher order behavior, I think we now have an amalgamation of formally verified concepts that we can consider fast enough and sufficient exercised in practice that we are ever closer to widespread formally and dependably verified software. Still, it's a long journey, and academic formal verification would always be, by design, a few steps ahead of what the industry can do efficiently in practice.
  • Taikonerd 2mo ago
    The field really needs more popularizers. I mean people or projects who can do "advertising" like, "if you add our linter to your CI/CD pipeline, you'll never have X class of bug ever again!"
• rrook 2mo ago
  given your experience on the topic, i'm curious: do you think that the reason we haven't figured out how to make other parts of formal verification fast is that, in general, programming languages expose each individual machine operation in the code, so the verification surface area is the combinatorial set over that? i've been working on a low level high opinion language, and its verifications are able to be checked in an extremely tight loop, largely because of the structure of the language itself.
• marcosdumay 2mo ago
  Or, at least how to make easy to create. (What is related to fast in complex ways.)