Fix segfault in MKSTR

Can't assume that the string resulting from an FFI call is not null!
The RTS generally assumes strings are not null later, however, so it's
important to test.
tutorial ffi: add emphasis

Add emphasis to 'target' in the examples so the string 'target' doesn't
get confused with concrete syntax:

    %include target "x"
tutorial: fix typos, add additional step to proof

An additional step is needed to prove plusredZ_S, namely compute.
tutorial: update interactive proof

Update interactive proof so it matches what one would get at the moment.
Merge pull request #519 from reynir/master

Update tutorial