News for hackers. Stuff that matters.

A comment on Haskell Problems for a New Decade. Parent comment

Re:Haskell Problems for a New Decade by agentultra on Friday January 24, 2020 @07:17PM (#22143606)
I think I mistyped. Pardon the pun!

I meant that Lean, I think, could be implemented in Lean.

Do you also work with Lean?

[ Parent | on HN ]
Re:Haskell Problems for a New Decade by Cladode on Friday January 24, 2020 @07:26PM (#22143641)
That's an interesting question: can Lean be implemented in Lean's dependent type theory.

I'm not currently working with Lean, but I will start a large verification project in a few months. We have not yet decided which prover to go for. We may write our own.

[ Parent | on HN ]
Re:Haskell Problems for a New Decade by agentultra on Friday January 24, 2020 @09:12PM (#22144185)
That sounds like it could be a lot of fun! Good luck. :)
[ Parent | on HN ]