I have recently given a talk on how we verify parts of GHC using hs-to-coq. The video of my talk is available at https://youtu.be/1NA6yV3cxNY :smile:

Nice! do you have the slides available too?

Sure! Slides available here: https://drive.google.com/file/d/1Cj7ax-b-BsWZeZ-fRFTu3BMdLUsWNfos/view?usp=sharing

Very nice. Did you get any response from the haskell community?

BTW what is the current thinking about Equations. E.g.

https://github.com/antalsz/hs-to-coq/issues/138

@Yao Li maybe this is a long shot, but any thoughts/hope for formalizing the core GHC language and connecting it to hs-to-coq? This (GHC core, https://github.com/ghc/ghc/tree/master/docs/core-spec) seems to be the closest Haskell has to any formal specification - it's in the Ott language, which can be used to generate a Coq definition with proper annotations

@Bas Spitters Yes. Some nice responses from the Haskell community. Most responses I've got are about how we translate Haskell to Coq (e.g. how do we handle laziness?). Simon PJ is also interested in if formalization can help write better code, which I'm also interested in but I haven't had a good answer to it.

If anyone has some interesting Haskell programs that they want to verify, or if any other ways of using hs-to-coq, I would love to hear about it!

As for Equations, I haven't heard much about the updates, either.

@Karl Palmskog Good question! And it is indeed something that we are trying to verify. For example, here is the Coq translation of the `CoreSyn`

module (together with a few other modules that `CoreSyn`

has mutual dependencies with) in GHC 8.4.3: https://github.com/antalsz/hs-to-coq/blob/master/examples/ghc/lib/Core.v You can find the `Expr`

data type on L651. And what we have proved is some properties about well-scopedness of term substitution, etc.

However, I don't think we can give a complete specification of Core and verify it because that is a lot of work.

ah, nice, thanks for the pointer

Is this the same formalization as the Deep Spec one? https://deepspec.org/entry/Project/Haskell.20CoreSpec

Ah, guess yes — Antal Spector-Zabusky is involved in both :-)

Yes it's the same one :)

Any thoughts on the interaction with liquidhaskell (we discussed it before in the issues), but LH seems to be gaining some traction now.

@Bas Spitters do you know how Liquid Haskell is connected to Haskell semantics, if at all? There are many claims to this effect in the Liquid Haskell papers, along the lines of "Liquid Haskell proves termination of a [Haskell function]", but from what I can tell what language you are verifying and whether this is something resembling Haskell is something that has to be taken by faith.

What worries me in particular is that there seems to be many Haskell functions which are known to not be verifiable by Liquid Types, even on pen and paper (see ICFP '14 paper).

They have a totality checker in LH, at that point the semantics is the same as for hs2coq.

Famously, haskell does not have a formal semantics, but one can more or less trust the total part.

I would disagree that just Haskell + totality gives you something reasonable, in the presence of the IO monad and the like. What I think LH should have done is to define an explicit Haskell fragment where they are sound. "Projecting" Coq functions to/from a messy language is at least a process that is amenable to inspection/analysis, and you can always fall back on Coq to fully define everything.

"total haskell is reasonable coq" is the premise of hs2coq.

https://arxiv.org/abs/1711.09286

I don't know how LH interacts with IO, I guess there is more in either the book, or in Niki's thesis.

https://ucsd-progsys.github.io/liquidhaskell-tutorial/

Did you check?

this looks like the closest on soundness there is: http://goto.ucsd.edu/~nvazou/thesis/main.pdf#page=143 (but not clear to me what the connection to Haskell/GHC is)

but more practically, perhaps @Yao Li could comment on whether Liquid Haskell devs have shown any interest in the Haskell Core Spec work? To me, a connection to something like this would be the obvious way to achieve trustworthiness for LH.

I haven't been in any discussion on that topic with the LH team. I think there might be some challenges of making connections between LH and CoreSpec: (1) a complete verification of Core is a lot of work, and (2) GHC is constantly evolving (even the parts relevant to Core). I would be concerned that a small team of hs-to-coq devs might not be able to verify enough Core to actually help make LH more trustworthy.

@Bas Spitters And what sort of connection do you have in mind? (Sorry I do not recall the earlier discussion. Maybe I didn't join the discussion.)

@Yao Li I just checked, it was an email discussion with some hs2coq developers.

In any case, then we saw two main hurdles:

- hs-to-coq uses GHC to parse and resolve names; but Liquid Haskell is not built into this machinery, and parses the LH annotations separately. So a non-trivial amount of plumbing would be needed to get our hands on the information we need.
- LH puts all the refinement type obligations of a Haskell function into a single SMT task. This may allow for more interaction between the equations than Program mode, where each occurrence of a refinement type would have to be solved individually.

thanks for the summary, this in my mind means that anyone who is "foundationally conscious" would focus on primarily using hs-to-coq for practical Haskell verification at the moment

I think it was nice what the VeriFast developers did, they basically carved out minimalistic fragment of their system and verified it end-to-end: https://people.cs.kuleuven.be/~bart.jacobs/fvf/ --- something like this should be within reach with CoreSpec + LH.

Yes, I was thinking along the same lines, but then I was told about the two hurdles above.

On the first hurdle, things might be easier now because LH is more integrated into GHC (but I haven’t watched the talk): https://icfp20.sigplan.org/details/hiw-2020-papers/1/Liquid-Haskell-as-a-GHC-Plugin

Last updated: Feb 06 2023 at 05:03 UTC