Lefteris Karapetsas

Use a prover like [why3](http://why3.lri.fr/) in order to provide the ability to prove invariants about the logic of functions of the language in compile time.

Implement the ability to load the Refu Intermediate format from a file.

Implement the ability to save the Refu Intermediate format to a file.

This is a design decision that I am not so sure about. At the moment almost all of the backend llvm functions take the `llvm_traversal_ctx` as an argument. Example [here](https://github.com/refu-lang/refu/blob/df6b362ca627d2a20fda8cd43957bca390cfd3dc/src/backend/llvm_ast.c#L55)....

Some ast headers contain inline functions and need to [include ast/ast.h](https://github.com/refu-lang/refu/blob/df6b362ca627d2a20fda8cd43957bca390cfd3dc/include/ast/function.h#L6) for various reasons. This can be sort of ugly and in addition can create danger of circular dependencies. Figure...

At the moment we only have a syntactic prefix increment and decrement operator `++` and `--` which acts like a postfix operator. Think on whether we also want the postfix...

Many of the type operators should have the associative property. As an example the sum type: `string | i32` is the same as `i32 | string` and yet the current...

Check all `bllvm_compile_XXX()` function's error path returns and make sure so that all errors can be handled a bit more gracefully. Example function [here](https://github.com/refu-lang/refu/blob/df6b362ca627d2a20fda8cd43957bca390cfd3dc/src/backend/llvm_ast.c#L142). Errors here are fatal, but still...

At the moment tests only exist for [proper scanning](https://github.com/refu-lang/refu/blob/df6b362ca627d2a20fda8cd43957bca390cfd3dc/test/lexer/test_lexer.c) of tokens, but not for the lexer unhappy cases. Make some new tests for the lexer errors and assert also that...

Sum types that are permutations of one another should have same unique key.