Skip to content

Blog

Rzk Formatter

Version 0.7.0 (and later 0.7.3 with bug fixes) of Rzk has recently been released, and it brings with it an exciting new feature: the auto formatter! It has been under work for over 3 weeks and came with unique design challenges that I will attempt to unpack in this post.

We have a blog now!

This weekend I have spent some time to make some updates to the Rzk website. In particular, we now have multi-lingual support (with some significant portions translated to Russian) as well as a blog system, where we plan to regularly post about changes and improvements to Rzk, tooling, and related formalization projects.

The blog supports literate Rzk files:

#lang rzk-1
#define hello-world
  : U
  := (hello : U) → hello