Quite. It's the silliest of silly ideas - not just practically, but conceptually, because real problems don't have hard algorithmic edges. Which is why they're so hard.
Don't forget there's a difference between a formal (user) specification and a functional specification.
A functional specification says that when you select "Edit -> Cut" the user can expect certain things to happen. A formal specification defines how the symbolic entities involved in implementing the operation should operate.
This isn't too hard for "Edit -> Cut", but it's not tractable at all for "Translate this poetry into another language without mistakes or ambiguities."
So in fact he's just as guilty of resorting to metaphor as anyone else in computing. Only in this case the metaphor is the algorithmic perfection and consistency of a mathematical proof.
This is fine in the classroom and in certain applications where formal methods can help, but not so much in the average developer room.
It also highlights that ultimately computers aren't about manipulating symbols, but about manipulating conceptual metaphors represented by symbol sets.
But I expect he'd have dismissed that idea as too dangerously novel.
>It also highlights that ultimately computers aren't about manipulating symbols, but about manipulating conceptual metaphors represented by symbol sets.
Not quite. Computers only deal with Symbolic Logic via Formal Systems. The mapping of those to a Domain of Discourse is the job of the Programmer.
Don't forget there's a difference between a formal (user) specification and a functional specification.
A functional specification says that when you select "Edit -> Cut" the user can expect certain things to happen. A formal specification defines how the symbolic entities involved in implementing the operation should operate.
This isn't too hard for "Edit -> Cut", but it's not tractable at all for "Translate this poetry into another language without mistakes or ambiguities."
So in fact he's just as guilty of resorting to metaphor as anyone else in computing. Only in this case the metaphor is the algorithmic perfection and consistency of a mathematical proof.
This is fine in the classroom and in certain applications where formal methods can help, but not so much in the average developer room.
It also highlights that ultimately computers aren't about manipulating symbols, but about manipulating conceptual metaphors represented by symbol sets.
But I expect he'd have dismissed that idea as too dangerously novel.