5 ms·

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

by dorfsmay 2y ago

garbthetill 2y ago
may i ask why isabelle over agda or lean?
- dorfsmay 2y ago
  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!
  - hwayne 2y ago
    [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 https://github.com/hwayne/lets-prove-leftpad [/invalid closing tag]
- chaoskanzlerin 2y ago
  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.
fspeech 2y ago
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 https://github.com/htzh/holnat), which, while slightly less pretty, makes loading and reloading significantly faster.
- dorfsmay 2y ago
  Thanks. There's also https://github.com/jrh13/hol-light https://github.com/jrh13/hol-light which I think is still maintained (just learned about it in https://www.youtube.com/watch?v=uvMjgKcZDec https://www.youtube.com/watch?v=uvMjgKcZDec from this thread: https://news.ycombinator.com/item?id=40619482 https://news.ycombinator.com/item?id=40619482)

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

garbthetill 2y ago

may i ask why isabelle over agda or lean?

dorfsmay 2y ago
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!
- hwayne 2y ago
  [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 https://github.com/hwayne/lets-prove-leftpad [/invalid closing tag]
chaoskanzlerin 2y ago
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.

fspeech 2y ago

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 https://github.com/htzh/holnat), which, while slightly less pretty, makes loading and reloading significantly faster.

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