<commit_before>
![LiquidHaskell Logo](img/logo.png)

# Guarantee Functions are Total

<div class="example-row">
<p>
LH warns you that head is not total as it is missing the case for <code>[]</code> and checks that it is total on <code>NonEmpty</code> lists.
</p>
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-head.gif">
</div>

<div class="example-row">
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-unstutter.gif">
<p>
The input contract propagates to uses of <code>head</code> which are verified by ensuring the arguments are <code>NonEmpty</code>. 
</p>
</div>

# Keep Pointers Within Bounds

<div class="example-row">
<p>
LH lets you avoid off-by-one errors that can lead to crashes or buffer overflows. 
</p>
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-vectorsum.gif">
</div>

<div class="example-row">
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-dotproduct.gif">
<p>
Dependent contracts let you specify, e.g. that <code>dotProduct</code> requires equal-sized vectors.
</p>
</div>

# Avoid Infinite Loops

<div class="example-row">
<p>
LH checks that functions terminate and so warns about the infinite recursion due to the missing case in <code>fib</code>.
</p>
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-fib.gif">
</div>

<div class="example-row">
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-merge.gif">
<p>
<em>Metrics</em> let you check that recursive functions over complex data types terminate. 
</p>
</div>

# Enforce Correctness Properties

<div class="example-row">
<p>
Write correctness requirements, for example a list is ordered, as refinements. LH makes illegal values be <em>unrepresentable</em>.
</p>
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-ups.gif">
</div>

<div class="example-row">
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-insertsort.gif">
<p>
LH automatically points out logic bugs, and proves that functions return correct outputs <em>for all inputs</em>. 
</p>
</div>

# Prove Laws by Writing Code

<div class="example-row">
<p>
Specify <em>laws</em>, e.g. that the append function <code>++</code> is associative, as Haskell functions. 
</p>
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-assocthm.gif">
</div>

<div class="example-row">
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-assocpf.gif">
<p>
Verify laws via <em>equational proofs</em> that are plain Haskell functions. Induction is simply recursion, and case-splitting is just pattern-matching. 
</p>
</div>

# Get Started

The following links are a quick way to play with and learn about LH:

* [Try LiquidHaskell now](http://goto.ucsd.edu:8090/index.html) in your browser.
* Follow a tutorial:
    * The [Official Tutorial](https://ucsd-progsys.github.io/intro-refinement-types/120/) (long but extensive)
    * [<NAME>'s Tutorial](https://liquid.kosmikus.org) (short but incomplete)

For more links, see the nav-bar at the top of this page.

# Get involved

If you are interested to contribute to LH and its ecosystem, you may want to:

* Read the contribution [guidelines](contributing.md)
* Read our [developers' guide](develop.md) to LH
* Join the LH [community](community.md) to discuss issues related to LH
<commit_msg>Remove dead links<commit_after>
![LiquidHaskell Logo](img/logo.png)

# Guarantee Functions are Total

<div class="example-row">
<p>
LH warns you that head is not total as it is missing the case for <code>[]</code> and checks that it is total on <code>NonEmpty</code> lists.
</p>
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-head.gif">
</div>

<div class="example-row">
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-unstutter.gif">
<p>
The input contract propagates to uses of <code>head</code> which are verified by ensuring the arguments are <code>NonEmpty</code>. 
</p>
</div>

# Keep Pointers Within Bounds

<div class="example-row">
<p>
LH lets you avoid off-by-one errors that can lead to crashes or buffer overflows. 
</p>
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-vectorsum.gif">
</div>

<div class="example-row">
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-dotproduct.gif">
<p>
Dependent contracts let you specify, e.g. that <code>dotProduct</code> requires equal-sized vectors.
</p>
</div>

# Avoid Infinite Loops

<div class="example-row">
<p>
LH checks that functions terminate and so warns about the infinite recursion due to the missing case in <code>fib</code>.
</p>
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-fib.gif">
</div>

<div class="example-row">
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-merge.gif">
<p>
<em>Metrics</em> let you check that recursive functions over complex data types terminate. 
</p>
</div>

# Enforce Correctness Properties

<div class="example-row">
<p>
Write correctness requirements, for example a list is ordered, as refinements. LH makes illegal values be <em>unrepresentable</em>.
</p>
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-ups.gif">
</div>

<div class="example-row">
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-insertsort.gif">
<p>
LH automatically points out logic bugs, and proves that functions return correct outputs <em>for all inputs</em>. 
</p>
</div>

# Prove Laws by Writing Code

<div class="example-row">
<p>
Specify <em>laws</em>, e.g. that the append function <code>++</code> is associative, as Haskell functions. 
</p>
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-assocthm.gif">
</div>

<div class="example-row">
<img src="https://ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-assocpf.gif">
<p>
Verify laws via <em>equational proofs</em> that are plain Haskell functions. Induction is simply recursion, and case-splitting is just pattern-matching. 
</p>
</div>

# Get Started

The following links are a quick way to play with and learn about LH:

* [Try LiquidHaskell now](http://goto.ucsd.edu:8090/index.html) in your browser.
* Follow a tutorial:
    * The [Official Tutorial](https://ucsd-progsys.github.io/intro-refinement-types/120/) (long but extensive)
    * [<NAME>'s Tutorial](https://liquid.kosmikus.org) (short but incomplete)

For more links, see the nav-bar at the top of this page.

# Get Involved

If you are interested in contributing to LH and its ecosystem, that's great!
We have more information on our [GitHub repository](https://github.com/ucsd-progsys/liquidhaskell).

{'fraction_non_alphanumeric': 0.1464343242055938, 'fraction_numerical': 0.002050080538878313, 'mean_word_length': 4.734676742233417, 'pattern_counts': {'":': 0, '<': 153, '<?xml version=': 0, '>': 153, 'https://': 25, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3275626', 'n_tokens_mistral': 2459, 'n_tokens_neox': 2291, 'n_words': 668}