Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
I read somewhere that the Apollo Guidance Computer was designed in such a way, that, although it is hugely less powerful than the average smartphone, it was dependable to the point that it "never crashed". My questions pertaining to this were:
Is designing such a digital system possible, even in the '60's ?
What are the constraints that one would want to look out for when attempting to design such a digital system that "never crashed", using today's technology?
It wasn't possible back then, in the absolute sense. What you're essentially looking for when you say "never crashes" is a system that always makes progress towards its goals. Today, we can prove that a computer program does that, but the relevant methods to construct such proofs were only developed starting in the 70's - years after the Apollo Guidance Computer was developed.
Practically speaking, today we would formulate the requirements on the guidance computer using a formal specification language. In particular, we'd identify each task of the computer, and specify that each task finishes n a bound number of steps. We also define a task scheduler that never halts and chooses the right tasks for each stage of the mission. With a bit of work, we then prove that every task that needs to be executed is executed on time. We then transform the specification into code, in a way that allows us to verify the proof still holds.
