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

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.

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.

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

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.