It is purist, and that's hard for a general audience. To CS and math
people, this is exactly the way to go. The start is stronger. Some of
Ken Thompson's more worrying work should be included to convey our
intuitive fear of this to the layperson. The second link may not be all
that credible, but the story conveys what guix is meant to prevent, and fix.
http://wiki.c2.com/?TheKenThompsonHack
https://www.quora.com/What-is-a-coders-worst-nightmare/answer/Mick-Stute?srid=RBKZ&share=1
https://en.wikipedia.org/wiki/Backdoor_(computing)#Compiler_backdoors
I think some of the buildup to the logical proof can be omitted, with
just the assertion that with the elements of FLOSS, Reliability, and
Trust are required and guix is designed to guarantee those would be
sufficient for the audience.
