# Using dependent types to write proofs in Haskell | Ascetic Slug

**URL:** <https://discourse.haskell.org/t/using-dependent-types-to-write-proofs-in-haskell-ascetic-slug/2601>\
**Category:** Links\
**Created:** [June 2, 2021, 11:14pm UTC](https://discourse.haskell.org/t/using-dependent-types-to-write-proofs-in-haskell-ascetic-slug/2601 "2021-06-02T23:14:43Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![janmasrovira](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/janmasrovira/32/1128_2.png) [@janmasrovira](https://discourse.haskell.org/u/janmasrovira)\
**Post date:** [June 2, 2021, 11:14pm UTC](https://discourse.haskell.org/t/using-dependent-types-to-write-proofs-in-haskell-ascetic-slug/2601/1 "2021-06-02T23:14:44Z")

</div>

I wrote a blog where I explain how one can use GHC’s type system to write mathematical proofs.

[https://janmasrovira.gitlab.io/ascetic-slug/post/haskell-proofs/](https://janmasrovira.gitlab.io/ascetic-slug/post/haskell-proofs/)

---

<div class="post-metadata">

**Author:** ![reuben](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/reuben/32/4733_2.png) [@reuben](https://discourse.haskell.org/u/reuben)\
**Post date:** [March 13, 2022, 3:19pm UTC](https://discourse.haskell.org/t/using-dependent-types-to-write-proofs-in-haskell-ascetic-slug/2601/2 "2022-03-13T15:19:34Z")

</div>

I thought this was a really nicely written article.

---

<div class="post-metadata">

**Author:** ![romes](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/romes/32/2912_2.png) [@romes](https://discourse.haskell.org/u/romes)\
**Post date:** [March 13, 2022, 9:37pm UTC](https://discourse.haskell.org/t/using-dependent-types-to-write-proofs-in-haskell-ascetic-slug/2601/3 "2022-03-13T21:37:22Z")

</div>

Really cool! Thank you