Comment by rtpg | Hacker News Reader

Comment by rtpg | Hacker News Reader

Parent Full thread

I think that Coq/Agda/Lean and friends are really going to be the winners in the proof space. Interactivity is a pretty good model for the feedback loop, and they're systems that exist and work, without a lost of asterisks.

The biggest thing I think these tools are missing out of the box is, basically, "run quickcheck on my proof for me". It's too easy to have some code, and try to prove some property that isn't true, and rip your hair out thinking "why can't I get the proof working!"

If halfway through your proof you end up in a thing that seems nonsensical, it would be nice for these tools to just have a "try to generate a counter-example from here" command that spits out a thing.

Proofs are so path-dependent, and it's not trivial to do in general. But I think they are all very close to greatness, and every time I've gone through the effort to formally verify a thing, it's been pretty illuminating. Just... if you're trying to prove some code, the process should take into account the idea that your code might be buggy.

I also quite like Idris, the problem with these languages is that they require being a Mage level 10, while most folks are still getting around magic exists.

I found the onboarding to be super rough… I think it’s the sort of thing where you really want to do a full day workshop on it to get started.

The interactive elements really can’t be done justice in looking at readme’s or textbooks alone IMO

In my case (Lean), I've been getting a lot of help through the Zulip community. There's a dedicated #new_members stream where anybody can ask total beginner questions. It's quite humbling actually when you have someone like Kevin Buzzard answering your noob questions.

I'm sure other solvers (Coq, Idris, etc.) also have online communities where you may be able to ask questions.

I'll have to agree with this. In particular, there always seems to be some stage where you'll have to think carefully about how the simplifier works exactly, about different types of equality (syntactic vs. definitional vs. provable), etc. And changing internal representations of objects will also mean that old proofs might not compile anymore. And tactics are often rather opaque blackboxes.

I say this as a non-expert who has been enjoying writing some Lean recently and has previously also written some Coq and Idris.

Most programmers don't have enough previous experience proving things so this is unnatural for them. It is sadly impossible to require programmers to have been a math major to get them the mental facility to work with these languages.

At my university, all majors of computer science have to take a course in discrete math, which involves writing a couple different types of math proofs using proof by induction (including strong induction) and proof by contradiction. However, that was the only class I've ever taken where I've had to write proofs regularly.

Anyway, I think that, at a minimum, at least one class like that should be part of every CS major's education, if it isn't already. That way, proofs are less intimidating, and things like Coq and Isabelle/HOL are less intimidating.

I agree with you, but the ship has sailed to retroactively require all programmers to have such experience. Also, the typical introductory discrete math course likely doesn't require writing proofs in a language precise enough to be formalized. I would think that we need at least one more introductory course to logic (first order logic, Peano axioms) and an introductory course to type systems (structural induction, progress and preservation, etc).

We also learned some first order logic, enough to write the proofs in formal language, though we didn't learn anything about type systems.

You're probably right about the ship having sailed, though. It's probably harder to get people to learn new things when they haven't been in school for a long time.

Isabelle/HOL has Quickcheck, which is precisely what you think it is. Although it only works if the free variables in the thesis you'd like to prove are sufficiently simple AFAIK (think integers or lists). The more powerful alternative to Quickcheck is Nitpick, which is a purpose-built counterexample finder.

The workflow you'd like already exists one to one in Isabelle: You can simply type "nitpick" halfway through a proof and it will try to generate a counterexample in that exact context.

> "try to generate a counter-example from here" For the theories behind some SAT solvers, that's quite possible. There's a set of problems that are completely decidable. These are composed of add, subtract, multiply by constants, logic operators, and theory of arrays and structs. That covers most things which cause programs to crash and many of the things you want to write in assertions.

Reply on news.ycombinator.com