Hacker News Reader

Comment by danharaj | Hacker News Reader

Synthetic differential geometry formalizes calculus in a way that precludes most monsters. Quite nicely, it allows you to use infinitesimal reasoning. The price to pay is the law of excluded middle. If you're a programmer, you're probably fine giving that up.

The wiki page has good references: https://en.m.wikipedia.org/wiki/Synthetic_differential_geome...

View on HN

Oh. I'm happy someone brought this up!

For anyone interested, Anders Kock has a nice slim-but-dense book on the subject entitled "Synthetic Differential Geometry" [0]. Kock even offers a PDF of an older version [1] on his site.

[0] http://a.co/717X9pE [1] http://home.imf.au.dk/kock/sdg99.pdf

"The first is that most of the analytic data for describing the class of smooth manifolds can be encoded into certain fibre bundles on manifolds: namely bundles of jets (see also jet bundle)."

Oh, mathematics, you are crazy.

This is a technically precise, compact way of saying "most of what we care about of smooth manifolds is how differential equations on them behave locally and how that local information can be glued together".

Yeah this kind of nullifies the pull quote

> If Newton had known about such functions, he would have never created calculus.

since Newton did use infinitesimals in his reasoning.

Only if you are that exceedingly queer kind of programmer who thinks that which is not within reach of Coq can never be truth.

I am a programmer, but I like C better, and assert(A && !A) looks like a monster to me.

Well, you probably meant assert(A || !A), but even so that will of course never be an issue if A is a value, it becomes only a problem if A is replaced by something like a() (which I assume to be a pure function for the purpose of this comment). Of course a() || !a() is never going to be false either, so assert(a() || !a()) will never abort your program, but that doesn't mean a() || !a() will ever be true (if a() never finishes calculating then neither will a() || !a()).

(A && !A) is always false even if (A || !A) isn't justified . In other words, !!(A || !A).

When we reject excluded middle we are no longer talking about truth, but evidence.

Reply on news.ycombinator.com