Thanks for taking a look. I agree that it is REALLY challenging (and currently impossible) to maintain that kind of formality in most codebases. Where it matters, though, it really helps.
I got interested in formal verification in the context of a future (currently vaporware 😅), formally verified version of the Cardano node running on a Formally Verified flavor that utilizes the RISC-V architecture. I’m just trying to put it on the white beards’ radar over there at IOG (it’s WAY out of my wheelhouse and perhaps even many of theirs too!) because this kind of thing, if fully open source (as that whole codebase is), could make this level of sophistication much more achievable by mere mortals.
Another amazing company that got me into this level of sophistication was Runtime Verification. If you like looking at projects that are absolutely world-changing, look into their K framework. They’ve created a whole framework for formally specifying whole programming languages (and even the LLVM!) and can pretty much use it as a Babel Fish for converting code from one programming language to another, which I always thought was impossible. But if there’s any outfit that could accomplish it, it might be those geniuses who regularly work with companies like NASA and aerospace behemoths.
Thanks for taking a look. I agree that it is REALLY challenging (and currently impossible) to maintain that kind of formality in most codebases. Where it matters, though, it really helps.
I got interested in formal verification in the context of a future (currently vaporware 😅), formally verified version of the Cardano node running on a Formally Verified flavor that utilizes the RISC-V architecture. I’m just trying to put it on the white beards’ radar over there at IOG (it’s WAY out of my wheelhouse and perhaps even many of theirs too!) because this kind of thing, if fully open source (as that whole codebase is), could make this level of sophistication much more achievable by mere mortals.
Another amazing company that got me into this level of sophistication was Runtime Verification. If you like looking at projects that are absolutely world-changing, look into their K framework. They’ve created a whole framework for formally specifying whole programming languages (and even the LLVM!) and can pretty much use it as a Babel Fish for converting code from one programming language to another, which I always thought was impossible. But if there’s any outfit that could accomplish it, it might be those geniuses who regularly work with companies like NASA and aerospace behemoths.