Hi everyone 
. I like the concept of Scala that fuse together math and coding (I love both of it!). I found out that DOT (Dependent Object Type) is the foundation of Scala 3 and research on this topic by reading:
The Essence of Dependent Object Types from EPFL
and
However it is too hard for me to fully understand all of it . Can anyone please explain the pros and cons of the DOT over the other type system of the other programming language?
Welcome to Scala!
Your question opens a very big space to try and cover. Like such a big space, the answer might not be useful to you.
So, can you narrow down the area a bit by saying why you want to know this? And perhaps identify a language or two with which you are familiar upon which one could base the contrast and comparison? That would help make generating an answer much more tractable and concrete which likely would be far more useful to you and to others who end up reading this thread.
Definitely!
At first, from many resources such as dotty fact, essence of scala or stack overflow depict that DOT is heavily researched in the past several years in order to create and improve new scala. (I love this kind of things like how rust has invented Ownerships and Borrowing rules to discard the garbage collector 
).
From the resources and papers, my curious is boiled down to 2 main questions.
Given the resources you have already listed, Iām not sure thereās much to add.
For your first bullet, the article, āEssence of Scalaā, starts with the āDOT Calculusā. I donāt know where you could find a discussion about how thatās related to the more Mathās general notion of ācalculusā. Perhaps someone who was involved in the DOT proofs could show an explicit connection.
For your second bullet, it appears all three articles you cited provide first approximation answers to your questions.
For example, Odersky outlines the elevated expectations of performance improvements because of the resulting simplification of internals. Whether that is from improved type soundness, or the many other Scala 3 adaptations and improvements over Scala 2, or both, itās not clear. And what benefit would there be from seeking clarification?
Were you intending to use Scala 3? Or are you researching it to consider as an option against other alternatives like TypeScript, Haskell, etc.? Or are you just a compiler theory enthusiast just kicking the Scala compiler tires as opposed to seeking to actually utilize it? Just trying to continue to narrow down what youāre actually seeking as your questions still left a very large abstract surface area.
Thanks for the answering 
.
It is not for comparison to choose the language for my profession or anything. I love many languages (mostly python, rust and scala!), it has its unique features and capabilities.
Most of the question just comes from my curiosity, it is just interesting (like how Rust introduce new concept!). It is as you said that the resource does point out the benefit, but not in the plain English 
, and thatās why I am trying to seek the answer from the Scala developer or the contributor here.
On thing to clarify (in case this was not clear): this is not āCalculusā in the sense of āDifferential and Integral Calculusā (i.e., the contents of a āCalculusā course), but in the sense of formal rules for calculating. So DOT Calculus is similar to (indeed perhaps a generalization of) Lambda Calculus in logic.
regards,
Siddhartha
If you mean ācalculusā as in the common math class with differentials and integrals, itās not. āCalculusā is a word with a broader meaning: āa method of computation or calculation in a special notationā. The calculus youāre probably familiar with is āinfinitesimal calculusā, but there are many other kinds of calculi, including DOT.
The main improvement from DOT is soundness. For a somewhat hand-wavy intuition, when a type system is sound that means you cannot represent an invalid program within the type system; if it passes the type checker, then it is correct in some sense. It might not be logically correct where it does what you intended, but it is type-correct in that things are what they say they are, and you wonāt have an integer when you expected to have a string. In an unsound type system you can have code that passes the type checker but fails at runtime.
Thanks everyone, I get a glimpse of it now.
So, with the new DOT foundation, it is basically safer to code while maintain rich features of the Scala.