Profile cover photo
Profile photo
Andrej Bauer
Andrej's posts

It took me four years to write the paper "Five stages of accepting constructive mathematics", which is based on an eponymous talk I gave at the Institute for Advanced Study in 2013. The paper has been published in the Bulleting of the AMS. I hope you'll enjoy it! 

Post has attachment
In 2014 I gave a talk at TEDxUL. Finally I put in English subtitles. You'll have to turn them on by clicking on the CC sign.

Post has attachment

Post has attachment
The Foundations of mathematics (FOM) mailing list, which I left a while ago due to unfair moderating practices, seems to have gone crazy with infinite discussions of "Set theory versus Homotopy Type Theory".

I find the whole activity ridiculous and based on the false premise that the two foundations are in opposition (as attested by the titles of discussion threads), or that they cannot co-exist, or that all foundations of mathematics need to be linearly ordered. These are all childish and false motivations.

The discussions are further hampered by the fact that no expert in homotopy type theory is taking part. This might partly be a consequence of the lessons learned in the 1990's when FOM was extremely hostile to category theorists, although I suspect (and can affirm for myself personally) that the questions asked and the issues raised by Harvey Friedman are simply not relevant to the HoTT crowd. There seems to be a very fundamental difference in perception of what foundations of mathematics are, ought to be, and what purpose they serve.

Supplemental: I have deleted the extremely long comments that appeared under this post without reading them and have disabled further comments. I also deleted one paragraph of my post which was arguably something that required a reply. I am simply not in the business of prolonging discussions with titles like "HoTT vs. ZFC" that present "challenges to HoTT" or "challenges to ZFC", etc. They are counter-productive and do not serve any purpose that would warrant them appearing on my posts. If anyone feels like producing yet more discussions, they are welcome to do so under their own G+ account. It is easy enough to reference this post. But do not expect me to participate, I simply wanted to express publicly my disappointment with the FOM contracting a very common Internet sickness.

Post has attachment
Very sad news indeed. Just last year Helmut and I connected after having spent time together at CMU in the 1990's. We started making plans to connect the Ljubljana and Vienna theoretical computer science groups.

I am at the MAP 2016 meeting in CIRM Luminy, listening to talks by people who work very hard to verify the numeric behavior of ODEs and other numerical computations formally with proof assistants and other computer tools. It is all difficult and they're investing amazing amount of work and knowledge (imagine having to formally prove in Coq that some piece of C code correctly solves an ODE).

Another family of talks is about trying to do numerics with guaranteed output precision (which requires intermediate precisions to adapt themselves). And that's horribly difficult to do as well.

In contrast, the usual floating-point calculations that everyone does in practice are "fast & loose". They results are computed, but people do not really know how correct they are, even though they pretend they do. But they don't! They do not prove their programs are bug-free, they do not actually calculate precise error bounds on their numerical methods, and they do not actually study what effects the rounding errors have.

Why is it that engineers and applied mathematicians need not actually know that they got it right? My personal explanation is that in our society the standards of proof and scientific correctness in general are much lower than we would like to think. We are quite willing to pretend that we know things which we do not actually know.

A main advantage of Google+ over Facebook is gone. It is showing me crap under the pretense that "people in my cricles plused it". Is there a way to turn this off? I want to see exactly and precisely the things posted by people in my circles, without whatever Google thinks I should see.

Suppose I have two numerals in Gödel's System T which are βη-equivalent. Are they identical and why?

#logic #typetheory

Post has attachment
What are the #Haskell  designers thinking?! They're just giving ammunition to the likes of +Robert Harper. Not that I am objecting, as always much enjoy his, uhm, critical appraisal of Haskell.

Post has attachment
Time to update your membership again.
Wait while more posts are being loaded