logoalt Hacker News

jeanpah • yesterday at 6:49 PM • 1 reply • view on HN

I remember those languages were used to verify an implementation, in space rockets code (uni teacher said). But maybe there is a way to build something perfect instead of veryfying the correct implentation?


Replies

pixl97 • yesterday at 7:39 PM

There are two different layers here. You have the binary layer, where software is written and works at on a theoretical level. Then you have the messy components that interact with reality at an analog level. This is why one of the first tenants of security is don't give anyone else access to your hardware.

But even that isn't a foolproof winning strategy. When you start digging deeply you realize we exist in the allegory of platos cave. The reality we experience is an emergent phenomenon related to the scale at which humans operate. Things that operate at a much smaller scale experience a completely different reality than you do. For example gravity becomes so insignificant it's like it doesn't even exist when you're small enough. At least for me it's not hard to imagine nano machines that infect the substrate of a CPU and farm all your secrets out on side channels, or any number of other things that are pure sci-fi at the moment.