Two very minor suggestions for the demo:

1. I don't know what the "Docxtemplater" button does, but it eats my document without warning and that's annoying.

2. It would be nice if the page came with some example .docx files we could see it work on.

I think that what matters here (and what I think is the natural interpretation of "not every real number is computable") is what the theory thinks is true. That is, we're working with internal notions of everything.