Comment by lelanthran | Hacker News Reader

Comment by lelanthran | Hacker News Reader

Parent Full thread

Cherry picking only the accurate prediction makes it seem like the predictor is really good!

Look at the rest of that quote:

> The human, computer pair, will also interactively suggest, confirm and fine tune specifications of mathematical properties and invariants at points in the the program.

That hasn't happened and as far as I am aware, is not even close.

> This will help the computer assistant to not only better understand the program but also to to generate real time, verification test runs using SAT technology,

Ditto.

> Interactive testing will eliminate whole classes of logic bugs, making most non ui code correct by construction.

Ditto..

So, 1 out of 4 predictions correct, which makes it worse than random chance?

Someone imagined an AI mathematician. What we've got is a parrot…

I don't know, some of that is at least starting to happen with Idris 2, though not in the exact way predicted: https://www.youtube.com/watch?v=mOtKD7ml0NU (Type Driven Development with Idris 2)

Short summary of linked video: when your type system is powerful enough you can restrict the set of possible implementations to the point that the compiler can make a decent guess as to what the program should be to satisfy the type signature.

Can you explain how this is worse than random chance?

It is, for people who think that the chance of meeting dinosaur on the street is 50% (you either do or don’t)

/s

Does that account for multiverses?

They're just using a flat prior, which is maybe inappropriate.

A flat prior over a probability space with only four possible events, but in reality there are of course many more possible events from which those four were originally picked.

Yes, if we're being pedantic then they were far off.

I was just pointing out something fun.

> That hasn't happened and as far as I am aware, is not even close.

Isn't that just the Rust borrow checker?

In terms of end result, yes, but not in terms of means.

Reply on news.ycombinator.com