One of earlier works combining high-security and functional programming was a security kernel for Scheme48:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.4...
http://mumble.net/~jar/pubs/secureos/
That was the Scheme mathematically-verified in VLISP project:
https://en.wikipedia.org/wiki/PreScheme
There was also a mathematically-verified, Scheme CPU:
http://www.cs.indiana.edu/pub/techreports/TR544.pdf
I imagine combining even these three components into an integrated systems would provide a lot more security and availability than the average desktop. The simplicity of the CPU might also aid in producing a NonStop-like solution for five 9's availability.