4 ms·

I wanted to like this talk. I started to like this talk. But when he jumps from talking about a problem in clear language to mathematical language, I felt he's

I wanted to like this talk. I started to like this talk. But when he jumps from talking about a problem in clear language to mathematical language, I felt he's gone so wrong. For me, there's no way "Set x to the smallest number >= to all elements of A" is clear to almost anyone in the world. And I was educated in formal logic at uni, taking an advanced, 3rd year course with like just 5 out of the 20,000+ odd students at a top UK uni. So a tiny percentage of a small percentage of the population have ever got exposed to that sort of logic. The (massive) mistake he's made is thinking logic and language is clear and concise. That changing the words somehow magically changes the meaning. It's not. I'm sure it works for him. It would not work for most of us that need to communicate clearly with other people, including programmers who are not aware of the full meaning of that sentence. It's not how most humans work, think or communicate. Part of many programmers job is to use language that is understandable. Using a specialist language of maths does not make the requirements any clearer for most people, just for mathematicians. Worse still, the sharp listeners amongst you would have noticed that having completely rewritten his "what" he almost immediately he said "most mathematicians agree that the smallest number...". Notice the "most". So his rewritten "what" is not even right for all mathematicians.

mrkeen 2y ago
Perhaps you agree with Lamport even harder than Lamport does. If your team is going to get together and implement "Set x to the smallest number >= to all elements of A", and you feel that that it's an ambiguous or incomplete description, then it's up to you guys to formalise what is meant - a programming activity - rather than just coding it. If it is as poorly-specified as you suggest, then someone on your team will think that they have correctly implemented it (tests and all!) but it will give the wrong answer in production.
lokar 2y ago
He has written and spoken a number of time about the need for more mathematical (which I think would include logic and metalogic) education and thinking in CS If all programmers/ software engineers had a reasonable level of mathematical formalism (could understand and write proofs), and some amount of formal logic, that would be much better. I think that is his position Also, understand this is coming from one of the most prominent living people in the field. People ask him for his opinion about this stuff, so he shares it.
- mattmanser 2y ago
  In reality that is a waterfall process disguised as programming advice. What that is saying is that if only you really specified in a clear technical language the code, you wouldn't need to write much of it. It's like his version of UML. But it all boils down to what we know doesn't work, a waterfall development process. But worse still, it's a waterfall process where no-one outside a small clique, those who can speak the special language, can join in the design process.
MITSardine 2y ago
To be pedantic, the definition is wrong too. His definition is not the max but the supremum: - max: largest element that is in the set, if it exists - sup: smallest element larger than all elements in the set But he doesn't really use the definition he gives anyways, his invariant to prove correctness does not rely on it.

mrkeen 2y ago

Perhaps you agree with Lamport even harder than Lamport does. If your team is going to get together and implement "Set x to the smallest number >= to all elements of A", and you feel that that it's an ambiguous or incomplete description, then it's up to you guys to formalise what is meant - a programming activity - rather than just coding it. If it is as poorly-specified as you suggest, then someone on your team will think that they have correctly implemented it (tests and all!) but it will give the wrong answer in production.

lokar 2y ago

He has written and spoken a number of time about the need for more mathematical (which I think would include logic and metalogic) education and thinking in CS If all programmers/ software engineers had a reasonable level of mathematical formalism (could understand and write proofs), and some amount of formal logic, that would be much better. I think that is his position Also, understand this is coming from one of the most prominent living people in the field. People ask him for his opinion about this stuff, so he shares it.

mattmanser 2y ago
In reality that is a waterfall process disguised as programming advice. What that is saying is that if only you really specified in a clear technical language the code, you wouldn't need to write much of it. It's like his version of UML. But it all boils down to what we know doesn't work, a waterfall development process. But worse still, it's a waterfall process where no-one outside a small clique, those who can speak the special language, can join in the design process.

MITSardine 2y ago

To be pedantic, the definition is wrong too. His definition is not the max but the supremum: - max: largest element that is in the set, if it exists - sup: smallest element larger than all elements in the set But he doesn't really use the definition he gives anyways, his invariant to prove correctness does not rely on it.