alt Hacker NewsIt sounds like the crux of the issue here is that you don’t want formal verification in the first place. Your last paragraph sounds more like code contracts, which is also a thing that already exists.
It sounds like the crux of the issue here is that you don’t want formal verification in the first place. Your last paragraph sounds more like code contracts, which is also a thing that already exists.
Well, yeah, you have code contracts in Ada or Spec#, (very limited) fixed type ranges in Pascal, ... but no general purpose programming language lets you put an arbitrary expression in the same language in a type as a permanent condition, or lets you state facts that the compiler will prove.
Of course not, that would be equivalent to solving the halting problem, many people will say.
I wonder if that will change now: I'm happy with an imperfect sanitizer that I run every now and then and will run a couple of minutes and come back with: I've proved your conditions, I proved a violation, or I can't decide, please change your code.