I guess he means to approach stuff in a Lean 4 or like systems manner. Formally thinking about what you have while also verificating mathematicaly that everything works fine.
It was a nice opportunity to ask him how can he think more mathematically given foundational CS definitions are based on Turing machines that are much closer to the way a programmer thinks.
What? A Turing machine is a mathematical object that behaves according to well-defined rules. Also what definitions are you thinking about? Don't forget about the whole field of CS dealing with the lambda calculus.
@@tophy9865 Turing machines have mutable state, which makes them more natural for a programmer than a mathematician. Regarding lambda calculus, although equivalent to TM assuming CT Hypothesis, it’s not really used for practical CS eg. A PPT algorithm can’t be represented with vanilla lambda calculus and everyone just extends TM formalism. Additionally, Lamport is against type theory, which is how CS people are approaching mathematical foundations. Would be interesting to see how he approaches these topics.
@@atonal174 The lambda calculus is used for practical general purpose languages like SML and ocaml. I don't know what his views on type theory are tho.
I guess he means to approach stuff in a Lean 4 or like systems manner.
Formally thinking about what you have while also verificating mathematicaly that everything works fine.
It was a nice opportunity to ask him how can he think more mathematically given foundational CS definitions are based on Turing machines that are much closer to the way a programmer thinks.
What? A Turing machine is a mathematical object that behaves according to well-defined rules. Also what definitions are you thinking about? Don't forget about the whole field of CS dealing with the lambda calculus.
@@tophy9865 Turing machines have mutable state, which makes them more natural for a programmer than a mathematician. Regarding lambda calculus, although equivalent to TM assuming CT Hypothesis, it’s not really used for practical CS eg. A PPT algorithm can’t be represented with vanilla lambda calculus and everyone just extends TM formalism.
Additionally, Lamport is against type theory, which is how CS people are approaching mathematical foundations. Would be interesting to see how he approaches these topics.
@@atonal174 The lambda calculus is used for practical general purpose languages like SML and ocaml. I don't know what his views on type theory are tho.
@@tophy9865 lamport.azurewebsites.net/pubs/lamport-types.pdf "Should Your Specification Language Be Typed?
"
*MATHEMATICAL THINKING* 😊
how do I escape the box 😭
Kouini transistors
lol
In Jesus' Name Amen ✝️
so mathematical thinking in this context means thinking that does not make sense. gotcha.