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.

▲

captainmuon 4 hours ago | parent [-]

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.

▲

IsTom 4 hours ago | parent [-]

> 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.

	▲	gf000 an hour ago \| parent [-]
		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.