Anonymous
6/12/2025, 1:46:29 PM
No.105570643
>>105564145
>a lot more applicable than 'muh memory safety'.
I think that's not correct (or at least depends on what you mean by "memory safety").
If you mean something static (Rust, affine types, linear types) that's actually pretty close to formal verification, because static type systems already _are_ formal verification. They prove the absence of certain errors at runtime. Usually it's about lack of type errors (think string to int addition), but you can also guarantee that every resource (allocated memory, file descriptor, db connection) is eventually closed and closed only once, or that there is at most one mutable reference to the object.
Also see Curry-Howard correspondence linking types with theorems and programs with proofs. You can make your type system more and more powerful (cf. Barendregt's λ-cube) and eventually you can specify and prove arbitrarily complex properties (and in process you lose nice features like type inference).
And properties like "memory safety" or "lack of type errors" are both relatively simple to check and important for bug prevention - that's why we have relatively widespread languages that enforce them. On the other hand, full correctness proofs are really really expensive (in terms of development speed), require knowledge of weird math and honestly rarely needed. As an example of "expensiveness", you know the algorithm to check that parentheses are balanced, right? Trust me, proving this (in both directions, formalized here https://www.codewars.com/kata/5de1761596cc1d002d5e5d0a) is really hard, took me several days. And yet just coding the algorithm takes at most 15 minutes and after some testing you're 99.999% certain that you made no errors.
>>105570559
You can add possible bitflips in the semantics of your language, though it will be cumbersome.
>a lot more applicable than 'muh memory safety'.
I think that's not correct (or at least depends on what you mean by "memory safety").
If you mean something static (Rust, affine types, linear types) that's actually pretty close to formal verification, because static type systems already _are_ formal verification. They prove the absence of certain errors at runtime. Usually it's about lack of type errors (think string to int addition), but you can also guarantee that every resource (allocated memory, file descriptor, db connection) is eventually closed and closed only once, or that there is at most one mutable reference to the object.
Also see Curry-Howard correspondence linking types with theorems and programs with proofs. You can make your type system more and more powerful (cf. Barendregt's λ-cube) and eventually you can specify and prove arbitrarily complex properties (and in process you lose nice features like type inference).
And properties like "memory safety" or "lack of type errors" are both relatively simple to check and important for bug prevention - that's why we have relatively widespread languages that enforce them. On the other hand, full correctness proofs are really really expensive (in terms of development speed), require knowledge of weird math and honestly rarely needed. As an example of "expensiveness", you know the algorithm to check that parentheses are balanced, right? Trust me, proving this (in both directions, formalized here https://www.codewars.com/kata/5de1761596cc1d002d5e5d0a) is really hard, took me several days. And yet just coding the algorithm takes at most 15 minutes and after some testing you're 99.999% certain that you made no errors.
>>105570559
You can add possible bitflips in the semantics of your language, though it will be cumbersome.