I'm a co-author on the abstract linked in the comments but I'm coming from the computer science side so I'm not an expert on the models and I know very little classical differential geometry.

I had the same question and my current understanding is that

Differential Cohesion and Synthetic Differential Geometry have the same "canonical model": the SDG people use the Cahiers topos and Diff Cohesion people use the $\infty$-sheaves on the same site.

They are by no means equivalent: for instance Synthetic Differential Geometry axiomatizes a real line object $R$ and the Kock-Lawvere axiom uses it, whereas in differential cohesion the notion of "infinitesimal" distance is more "formal" in that it is just derived from abstract modalities. For instance there are very simple models of DC like this one that have a very strange notion of "infinitesimally close".

It's a matter of ongoing research how much differential geometry can be done using just differential cohesion, but clearly if you want to get all of the classical theorems you need to at some point axiomatize the reals (unfortunately any internal definition of the reals via Dedekind cuts will give you the wrong reals because you want to only have the smooth functions).

On the other hand Differential Cohesion is more "categorical" which syntactically means we hope to get well-behaved type-theoretic connectives instead of uninterpreted axioms, like how having the identity type in HoTT is much nicer than axiomatizing the n-spheres.

The main source for what can be formalized in (solid, differential) cohesion is Urs' book, look for the sections on the differential cohesion modalities to see some comparisons to SDG, but also note that much of that book can be formalized with just a cohesive topos.

For some shorter/simpler examples, see Felix Wellen's thesis if you want to see what some of differential geometry looks like using just one of the modalities from differential cohesion.
Also maybe check out Mike Shulman's paper for (non-differential) cohesion plus some axioms for a more hybrid style.

Also, when it comes to the infinity-stuff, I have been assured by experts that you can just ignore the word infinity when you are looking for intuition.
A big takeaway from infinity-category theory and Homotopy Type Theory is that infinity groupoids act a lot like sets.

3more comments