It’s interesting he discusses Liquid Haskell (proofs via refinement types) extensively:

“So, for me, that’s as far as increasing our ability to give you statically guaranteed theorems about Haskell programs. My money’s on Liquid Haskell at the moment and I hope that we the Haskell community”

It’s just an example of a single problem so it might be hard to extract very general conclusions. Also, standard libraries, and not proof frameworks, might dictate what is simpler in this particular case.

Wit that said, Idris is quite simple, but it’s dependently typed so it’s in a different class, with its own set of problems. Coq/SSReflect, Lean and Agda are also quite readable.

I really like Dafny, Frama-C and Java because they are extremely readable and conventional. Thanks to separation logic-like approaches, they are almost declarative.

I think the tl;dr is that proof automation is hard. Refinement types and Hoare logic scale better. This is why SPJ is more enthusiastic about these rather than dependent types.

I think with Dafny or WhyML you might be able to build non-trivial systems of ~20-40 KLOC in a couple of man-years, with high assurance. Doing this with Idris, Coq or Agda is not that easy right now.

Always great to hear SPJ, but even better is that it has a transcript! Thanks for that!

It’s interesting he discusses Liquid Haskell (proofs via refinement types) extensively:

“So, for me, that’s as far as increasing our ability to give you statically guaranteed theorems about Haskell programs. My money’s on Liquid Haskell at the moment and I hope that we the Haskell community”My experience is that other refinement type systems are way less complex. See solutions for a toy problem gathered by @hwayne at: https://github.com/hwayne/lets-prove-leftpad

In particular, compare https://github.com/hwayne/lets-prove-leftpad/blob/master/liquidhaskell/LeftPad.hs to https://github.com/hwayne/lets-prove-leftpad/blob/master/dafny/Leftpad.dfy. For me this has been a bit of a disappointment.

Thanks for this link. On quick perusal it looks like the Idris version is the simplest.

It’s just an example of a single problem so it might be hard to extract very general conclusions. Also, standard libraries, and not proof frameworks, might dictate what is simpler in this particular case.

Wit that said, Idris is quite simple, but it’s dependently typed so it’s in a different class, with its own set of problems. Coq/SSReflect, Lean and Agda are also quite readable.

I really like Dafny, Frama-C and Java because they are extremely readable and conventional. Thanks to separation logic-like approaches, they are almost declarative.

What are those? (I may spend some time learning Idris…)

Here they explain some: https://groups.google.com/g/idris-lang/c/7GmLjNKRuQ4

I think the tl;dr is that proof automation is hard. Refinement types and Hoare logic scale better. This is why SPJ is more enthusiastic about these rather than dependent types.

I think with Dafny or WhyML you might be able to build non-trivial systems of ~20-40 KLOC in a couple of man-years, with high assurance. Doing this with Idris, Coq or Agda is not that easy right now.

Oops, in retrospect I forgot

`audio`

and`transcript`

. Oh well.