2 ms·
I don't know who the target audience was, but I found the lecture very confusing and the message really badly passed (he keeps talking what is already written i
by jventura 8y ago
I don't know who the target audience was, but I found the lecture very confusing and the message really badly passed (he keeps talking what is already written in the slides, etc.). I had to play it at 1.6x the regular speed so I could move on with it.
Regarding the topic, I think there are multiple ways of expressing ideas, where math happens to be just one of them. For instance, for the Greatest Common Divisor example, you could just say that "if x equals y the cgd of x and y is x, else you need to keep subtracting the smallest number from the largest until both are equal".
You could use simple math, such as:
/ x if x=y
gcd(x,y) = | gcd(x-y, y) if x > y
\ gcd(x, y-x) if x < y
Or you could use code:
def gcd(x,y):
if x==y:
return x
elif x>y:
return gcd(x-y, y)
else:
return gcd(x, y-x)
In essence, what I want to say is that his definition of beauty and power may not match mine, but I will not argue that math can be more succinct or allow for better abstractions in many cases.
In the end, I got the feeling that he is trying to "sell" us his TLA+ approach.
- maccam912 8y agoI think he was trying to show that the TLA+ approach led to easier proofs of the base case and inductive case. I don't think he's arguing that your gcd program is bad. That's what I'd use. But TLA+ might be a good tool to break out when you need to have a solid proof that the code you wrote will always end up getting you the right answer. We probably don't need it for side projects, but it's nice to know that AWS has some proofs around that the services I use there can't end up in an inconsistent state as a result of any coding logic.
- deleted 8y ago[deleted]
- Apaec 8y agoCode doesn't have to look like that, look at the Haskell version: gcd x y | x == y = x | x > y = gcd (x - y) y | otherwise = gcd x (y - x) Much more close to the math notation.