Hacker News Reader

Comment by dorfsmay | Hacker News Reader

I just spent hours looking at formal methods and had decided to learn Isabelle/HOL, then this article !

I would recommend HOL Light and Lean. HOL Light is no longer being developed. It's very self contained and the foundation is very simple to comprehend. It's great for learning ATP, not the least due to the fact that Harrison wrote a nice companion book. And OCaml these days is very easy to access. I also developed a way to run it natively (https://github.com/htzh/holnat), which, while slightly less pretty, makes loading and reloading significantly faster.

Thanks.

There's also https://github.com/jrh13/hol-light which I think is still maintained (just learned about it in https://www.youtube.com/watch?v=uvMjgKcZDec from this thread: https://news.ycombinator.com/item?id=40619482)

may i ask why isabelle over agda or lean?

I know nothing, I am a complete beginner when it comes to formal methods. From reading about it, it seems that Isabelle/HOL is the best when it comes to automation which apparently is something you really want. It might be easier to learn (controversial, some say Lean is easier). It's been used to prove some software (including sel4 and a version of java), Apple and AWS are using it (but then I know AWS uses, or used, TLA+).

At the end of the day, I didn't want to spend more time reading about it then learning two of them (trying one and potentially switch later). The more you read about it, the more options open up (SPARK, TLA+, COQ, etc...).

I do find it ironic to read this article today given that I made that decision yesterday!

[shameless plug]I maintain a collection of proofs of leftpad in different prover languages, so people can compare them. It's here: https://github.com/hwayne/lets-prove-leftpad

[/invalid closing tag]

The main upside Isabelle has over other proof assistants is the existence of Sledgehammer: invoke it, and your current proof state gets handed off to a SMT solver like cvc4, veriT, z3, vampire, etc. If the SMT solver finds a solution, Isabelle then reconstructs the proof.

It's essentially a brute-force button that no other proof assistant (aside from Coq) has.

Reply on news.ycombinator.com