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.
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.
> 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
Lean can be used as a regular programming language. There's also languages like idris2 and f-star, but they don't seem to have much traction.
Well, they of course not defy computer science. The "trick" is that they are not Turing-complete, they mandate termination of every expression.
Also, most of them are made to prove stuff first and foremost and thus trade off a lot of performance to the point that it makes them practically unusable for many stuff (e.g. numbers may be represented as an object that has n-1 further children recursively), though Lean is an exception as you note.
> The "trick" is that they are not Turing-complete, they mandate termination of every expression.
I don't think this is a big deal for day-to-day programming. You're trying to stay in n, nlogn or maybe n^2 realm most of the time. And the kind of infinite loops you encounter (e.g. event loops) are co-inductive or have some notion of making progress.