WorCshop README

WorCshop is a VSCode extension for proving the correctness of C code as you write it.

Features

Right now, all it does is send the most recent line you typed to Coq at every newline and use Alectryon to render the resulting proof state.

Requirements

Requires Alectryon. Will also require VST eventually.