2 ms·
Specifying that a value must be an integer between 1 and 10 is most certainly further along the continuum than only specifying that a value must be an integer,
by win311fwg 3mo ago
Specifying that a value must be an integer between 1 and 10 is most certainly further along the continuum than only specifying that a value must be an integer, but both define a theorem about the program that can be validated. How is the latter not formal verification? It's the same thing, only differing by degree.
- IshKebab 3mo agoAs I said, it's a continuum. I'm drawing the line somewhere further along it than Rust's type system.
- win311fwg 3mo agoUnderstood. In dynamic verification, does that same line hold? Or would you say it is it unique to formal verification? If so, why?
- IshKebab 3mo agoFirst I've heard of "dynamic verification" tbh. Is that just everything that isn't static analysis? Not sure I understand the question!
- win311fwg 3mo agoYou may also know of it as standard verification or empirical verification. Regardless of the name, I am sure you can understand the concept as it is exactly of the same intent as formal verification (e.g. you might seek to ensure that a value is an integer between 1 and 10), but absent the formal methods. Of course, just as you can seek to verify that a value is between 1 and 10 you can also simply verify that a value is an integer. Therefore the possibility of the same dividing line exists in that space as well, but I was wondering if you recognize the same dividing line there, or if it is unique to where formal methods are used?