prepare release notes

CHANGELOG.md

@@ -1,9 +1,51 @@
 # Changelog
 
+Following is the changelog of Creusot, a verification tool for safe Rust programs. Using Creusot you can prove -- formally -- that your Rust program behaves in a specific manner.
+
+Creusot allows you to annotate your code using *contracts* which describe correctness conditions for your program. Creusot then uses SMT solvers to check that these contracts hold for all possible runs of the program. All of this is done statically without running your program, and contracts are erased at compilation time.
+
+Creusot is currently best suited for the verification of code like data-structures or algorithm implementations, and less so for systems which interact heavily with the outside world or exploit concurrency. Notable projects using Creusot include the [CreuSAT](https://github.com/sarsko/creusat) verified SAT solver and the [Sprout](https://github.com/xldenis/cdsat) SMT solver.
+
+**Creusot is still very experimental software, you should expect some obscure crashes and missing features.**
+
 <!-- next-header -->
 ## [Unreleased] - ReleaseDate 
 
+### Cargo Creusot
+
+Cargo creusot saw several minor improvements especially with regards to configurations.
+
+Users upgrading from `v0.1` will need to regenerate their configuration by running `cargo creusot setup install`.
+
+### Pearlite
+
+This release introduces the foundations of termination checking in Creusot by providing two new macros: `#[terminates]` and `#[pure]`.
+
+- `#[terminates]` indicates that a function terminates, these functions are allowed to crash or run out of memory.
+- `#[pure]` these functions are *total*, they must terminate and cannot exhibit *any* side-effects.
+
+The termination check generated by Creusot is currently overly conservative and does not support loops or mutally recursive functions.
+We expect to lift this restriction in future releases.
+
+While `terminates` functions may call either `pure` or `terminates` functions, `pure` can only call other `pure` functions.
+
+### Creusot Backend
+
+This change should mostly not be user-visible, but we want to disclose it both to encourage users to bring up any problems they encounter when moving to 0.2 and to share our vision for future releases.
+
+Version 0.2 marks the transition of Creusot to the new intermediate verification language [Coma](https://coma-ivl.codeberg.page/quickstart.html). Coma is designed as a modern kernal language for the Why3 platform and offers incredible flexibility while keeping an extermely minimal core. This replaces our usage of MLCFG in Creusot as the language we target.
+
+Using Coma we have a solution for the specification of closures which could allow us to elide significant portions of specifications in proofs.
+We don't currently leverage this, but expect it to be ready by version 0.3.
+
+We expect the primary noticable change to be a regression in the labels for proof tasks in logical functions, if you notice any other regressions including newly failing proofs, please report them on github.
+
+
+### Why3find support
 
+The code generated by Creusot was changed to be drop-in compatible with [`why3find`](https://git.frama-c.com/pub/why3find), an alternative cli-driven frontend for why3.
+You can run `why3find prove creusot_generated_file.coma`, so long as the directory this is run in contains a copy of the `prelude` folder of Creusot.
+Future verisons will integrate this natively into `cargo creusot`.
 
 ## [0.1.1]