It gets worse. Even if you write your OS in Haskell, how do you know your compiler hasn't been compromised? Or the hardware? The solution necessarily involves a social component, e.g. Haskell, with the development practices of OpenBSD (continuous re-auditing of everything including tools, complete openness, etc.) IOW, it'll never happen, but it might end up better than paper ballots.2009/2/19 Rick R <rick.richardson@gmail.com>I think the capabilities community including E and Coyotos/BitC have extensively addressed this topic. Coyotos is taking the correct approach for trusted voting platform. Since, even if your software is trustworthy, it can't be trusted if the OS on which it runs is suspect.Woah, that's a pretty interesting question! How do you write software which is protected against a malicious operating system (mind -- not erroneous, but rather somebody detecting the software you're running and changing your vote). Maybe some sort of randomized cryptographic technique, in which, with high probability, the OS either runs your program correctly or causes it to crash.