Comment by captainmuon | Hacker News Reader

Comment by captainmuon | Hacker News Reader

I haven't looked into Bend 2 in detail, but it seems a bit harsh to call it "horribly broken or decades behind the current state of the art". Clearly there is a problem with formal verification languages and there is a demand for something else in that area, and the problem is the usability and syntax. I don't want to have to learn something that looks like Haskell, or to have to wrap my head around Curry-Howard correspondence. I don't want to write my conditions in something that looks and feels like C++ template metaprogramming. I recall a Hello World in something like Coq a few years ago which basically started with "first, we construct the Peano integers", and then they used this to prove that some calculation was bounded - because it seems they couldn't represent integers natively?

I just want to be able to write C#, JavaScript or whatever, and then tack on preconditions, checks and so on with the same syntax. Dependent typing and design by contract for the masses.

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.

> "horribly broken or decades behind the current state of the art"

This is just about vibe-coded programs in general when the approach assumed by the article is taken. For all I know they did make an informed decision regarding the tradeoffs (which I would consider to be a poor decision).

> I just want to be able to write C#, JavaScript or whatever, and then tack on preconditions, checks and so on with the same syntax.

That's more or less what SPARK (and others) do, although specifications for large programs can become nasty.

Reply on news.ycombinator.com