Post

asa
@asap.systems

the more I learn about formal verification of software, the more absurd it becomes that it isn't commonplace in all mainstream software development

5 reposts37 likes

Sophie Kirschner
@pinemach.bsky.social

I'm so sorry did you think the purpose of software was to work and do things correctly and make the world a better place for people? My sweet innocent child, the purpose of software is to sell subscriptions

asa
@asap.systems

the ability to declare that a function only works for a specific set of inputs and set constraints on the outputs based on the inputs is awesome it's the same feeling as going from dynamic to static typing, you can encode the full invariants in your head onto the page

🅮☠𐱅 TOXIC CHLORAMINE GAS
@punishedtj.cryptoanarchy.network

Formal verification is ultimately nothing more than static typing with an extremely strong type system. As for why it's not more common, the answer is quite simply because it's hard. Proving useful properties about production-grade software is already an inherently hard task...

🅮☠𐱅 TOXIC CHLORAMINE GAS
@punishedtj.cryptoanarchy.network

But then you add on the fact that not all languages really support formal verification. Theoretically you could formally verify code in any language, but in practice you need it to have a formalized semantics for anything meaningful to come out of it, so there's basically only a few choices.