Zulip Chat Archive

Stream: general

Topic: DeepSpec summer school


view this post on Zulip Simon Hudon (Mar 11 2018 at 18:12):

The registrations are open for the DeepSpec summer school 2018: https://deepspec.org/event/dsss18/

Does anybody else intend to attend?

view this post on Zulip Andrew Ashworth (Mar 11 2018 at 18:25):

it looks interesting, but it seems participation is by invitation only, sadly

view this post on Zulip Andrew Ashworth (Mar 11 2018 at 18:26):

hopefully they will record lectures and post them online this year

view this post on Zulip Simon Hudon (Mar 11 2018 at 18:30):

But you can apply!

view this post on Zulip Moses Schönfinkel (Mar 11 2018 at 18:33):

Whoa... both Pierce and Chlipala, that's quite the "cast" they have :).

view this post on Zulip Andrew Ashworth (Mar 11 2018 at 18:33):

I am not a researcher in software certification though. It is unlikely they would accept me. I don't think interested amateurs get grant money :)

view this post on Zulip Simon Hudon (Mar 11 2018 at 19:13):

Is any of it relevant to your work? If the technology was mature enough, do you think you could make use of it?

view this post on Zulip Andrew Ashworth (Mar 11 2018 at 19:49):

as a programmer, when is software certification not relevant?

view this post on Zulip Andrew Ashworth (Mar 11 2018 at 19:51):

but yes, i first got interested in software certification when I was looking for help in automatically calculating error bounds on numerical algorithms, and then promptly realized it is super hard to work with floating point numbers

view this post on Zulip Andrew Ashworth (Mar 11 2018 at 19:52):

not to mention the theory is supremely tedious, i don't think anybody uses interval arithmetic in practice

view this post on Zulip Simon Hudon (Mar 11 2018 at 19:54):

I agree :) Let's put my question differently: how hostile is your industry towards verification? I have come to see that most employers look at verification with a lot of suspicion

view this post on Zulip Andrew Ashworth (Mar 11 2018 at 19:55):

pretty hostile, because proving things takes up many hours of expensive engineer time

view this post on Zulip Andrew Ashworth (Mar 11 2018 at 19:57):

it's far cheaper to sprinkle a few asserts here and there and do testing after the fact

view this post on Zulip Andrew Ashworth (Mar 11 2018 at 19:57):

i don't work in a safety-critical industry

view this post on Zulip Simon Hudon (Mar 11 2018 at 19:57):

Sometimes, that argument sounds like "using a computer is too expensive because writing our own OS and our own compiler takes way too much time"

view this post on Zulip Simon Hudon (Mar 11 2018 at 19:59):

But you have a point there: it's great when you can find a compromise like that. When the technology is mature, it's no longer a cost to use it. It really pushes you forward. I'm trying to sell Haskell that way.

view this post on Zulip Andrew Ashworth (Mar 11 2018 at 20:00):

I wake up every day and offer a small prayer of thanks to the various research funding bodies out there that allow people to spend time thinking about these things :)

view this post on Zulip Andrew Ashworth (Mar 11 2018 at 20:02):

but i think it's telling verification has only taken off in the hardware industry where making a mistake costs millions of dollars

view this post on Zulip Simon Hudon (Mar 11 2018 at 20:02):

I also have the same prayer :) it funds a great hobby of mine

view this post on Zulip Simon Hudon (Mar 11 2018 at 20:03):

What do you conclude from that fact?

view this post on Zulip Andrew Ashworth (Mar 11 2018 at 20:03):

a lot more work needs to go into automated theorem proving

view this post on Zulip Andrew Ashworth (Mar 11 2018 at 20:05):

also some mathematician somewhere needs to invent something more practical than interval arithmetic

view this post on Zulip Andrew Ashworth (Mar 11 2018 at 20:05):

these are both things I am wildly incapable of doing with my current skillset :)

view this post on Zulip Moses Schönfinkel (Mar 11 2018 at 20:05):

Careful about putting mathematician and practical in the same sentence! :)

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:32):

What's interval arithmetic?

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 20:32):

I don't think I've ever done anything practical.

view this post on Zulip Simon Hudon (Mar 11 2018 at 20:36):

Is it legal for mathematicians to do practical stuff? :stuck_out_tongue_closed_eyes:

view this post on Zulip Simon Hudon (Mar 11 2018 at 20:37):

Interval arithmetic is when you represent numbers as an upper bound and a lower bound on uncertainty and you do arithmetic on those bounds. When you need to round, you round down the lower bound and you round up the upper bound. That allows you to keep tack on the accumulated errors

view this post on Zulip Moses Schönfinkel (Mar 11 2018 at 20:38):

I think some take offense if you accuse them of doing something with practical applications.

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:39):

I don't take offense, I don't see what you mean.

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:39):

But I'm not a native English speaker

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:39):

Could you define "practical applications"?

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:39):

Never heard about this

view this post on Zulip Moses Schönfinkel (Mar 11 2018 at 20:40):

It's when your work is sub-par and not abstract enough.

view this post on Zulip Moses Schönfinkel (Mar 11 2018 at 20:40):

That's when some call it "practical".

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:42):

I found it. I knew I already met this "applied" word.

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:42):

It was in https://indico.math.cnrs.fr/event/1865/

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:42):

" On the foundational side, this concerns basics on the etale cohomology of diamonds including smooth and proper base change and Poincare duality, leading up to a good notion of "constructible" sheaves on the stack of G-bundles on the Fargues-Fontaine curve. On the applied side, this concerns the construction of (semisimple) L-parameters, the conjecture of Harris (as modified by Viehmann) on the cohomology of non-basic Rapoport-Zink spaces, and the conjecture of Kottwitz on the cohomology of basic Rapoport-Zink spaces."

view this post on Zulip Simon Hudon (Mar 11 2018 at 20:48):

Too down-to-earth for me

view this post on Zulip Simon Hudon (Mar 11 2018 at 20:49):

But what does it say about theorem prover developers that their practical application is helping mathematicians draw pies in the sky?

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:49):

Yeah, me too. That's why I'm not doing this arithmetic geometry stuff.

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:50):

I've been explained that theorem provers helping mathematician is an unwanted accident

view this post on Zulip Simon Hudon (Mar 11 2018 at 20:50):

Haha!

view this post on Zulip Simon Hudon (Mar 11 2018 at 20:51):

Formal methods have a really fun position where they get contempt from both practitioners and academics

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:55):

I don't have any contempt here

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:56):

(I don't even know how to build an English sentence using that word, my attempt sounds weird)

view this post on Zulip Patrick Massot (Mar 11 2018 at 20:58):

And, in case it's not clear: the story behind the quote with "foundational side/applied side" is that this talk announcement by the most fashionable abstract mathematician made mathematician laugh out loud everywhere it was seen, because the application mentioned is totally inside the world of abstract useless math

view this post on Zulip Simon Hudon (Mar 11 2018 at 21:20):

I don't see contempt here. It's just that I've been trying to promote the use of formal proofs for a while and I was expecting computer scientists to be excited to get rid of bugs and mathematicians to be excited to gain insight into their subject by the mere shape of their formulas but I've mostly been responded to by computer scientists like I was trying to build a perpetual motion system (unrealistic because of deep truths of the universe that they understand and that I don't) and by mathematician like I was building a huge steam powered machine to tie your shoes (overly grandiose and heavy handed approach to solve an easy problem)

view this post on Zulip Patrick Massot (Mar 11 2018 at 21:22):

It's certainly true that the vast majority of mathematicians are not yet convinced that proof assistants can be of any use to them

view this post on Zulip Patrick Massot (Mar 11 2018 at 21:22):

And it's true with the current state of proof assistants

view this post on Zulip Patrick Massot (Mar 11 2018 at 21:22):

but I hope this is changing

view this post on Zulip Patrick Massot (Mar 11 2018 at 21:23):

They only need to wait for Lean 4

view this post on Zulip Simon Hudon (Mar 11 2018 at 21:30):

I think this is a revolution happening slowly. Lean 4 will help of course but with Lean 2 and 3, preparation has been done. Even before that, with Coq and Isabelle, impressive projects have done. And as time passes, the required degree of expertise goes down. You no longer need to be Bertrand Russel to do a completely formal proof. You can even do it without a PhD these days

view this post on Zulip Simon Hudon (Mar 11 2018 at 21:31):

I keep hearing that the goals are impossible but milestones keep being reached regardless.

view this post on Zulip Patrick Massot (Mar 11 2018 at 21:33):

I'm not sure what is the next currently planned milestone on the math side of proof assistants

view this post on Zulip Patrick Massot (Mar 11 2018 at 21:33):

As far as I know, the previous one was the odd order theorem proof

view this post on Zulip Simon Hudon (Mar 11 2018 at 21:35):

I'm curious about the next one too. It might about formalizing subjects rather than individual proofs next. I'm more familiar with the ones in computer science

view this post on Zulip Patrick Massot (Mar 11 2018 at 21:52):

Since we already completely spoiled this thread. Let me ask an almost irrelevant question. I clearly don't care about this DeepSpec summer school. But what about that Oxford conference? Do you think it would useful to go there? How many people around here will go there?

view this post on Zulip Simon Hudon (Mar 11 2018 at 21:54):

Can you share a link?

view this post on Zulip Simon Hudon (Mar 11 2018 at 21:55):

(we could rename this thread to conferences and meetups)

view this post on Zulip Patrick Massot (Mar 11 2018 at 21:55):

https://itp2018.inria.fr/

view this post on Zulip Patrick Massot (Mar 11 2018 at 21:55):

Looking at the program of previous years doesn't really help

view this post on Zulip Patrick Massot (Mar 11 2018 at 21:56):

because 2016 talks seem to be very different from 2017

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 21:57):

That is a ridiculously large committee.

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 21:57):

Is it really such a gigantic area that they need a committee that big?

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 21:57):

Or do most people just do nothing?

view this post on Zulip Patrick Massot (Mar 11 2018 at 21:57):

To me it looks like the 2016 program would have been interesting to me but 2017 was too much CS

view this post on Zulip Patrick Massot (Mar 11 2018 at 21:58):

Of course it would also be fun if this could the opportunity to actually meet people from this forum

view this post on Zulip Patrick Massot (Mar 11 2018 at 21:59):

The committee is gigantic indeed

view this post on Zulip Patrick Massot (Mar 11 2018 at 21:59):

I've never heard of a conference with more organizers than speakers

view this post on Zulip Simon Hudon (Mar 11 2018 at 22:03):

That sounds like a really cool place to go. I wish I had a paper to present

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 22:05):

It seems to me that this CS world is just the same people organising conference after conference

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 22:05):

It seems very different to the maths world

view this post on Zulip Andrew Ashworth (Mar 11 2018 at 22:05):

That sounds like a really cool place to go. I wish I had a paper to present

In addition to regular papers, described above, there will be a section for shorter papers, which can be used to describe interesting work that is still ongoing and not fully mature. Such a preliminary report is limited to 6 pages and may consist of an extended abstract. Each of these papers should bear the phrase “(short paper)” beneath the title, and will be refereed and be expected to present innovative and promising ideas, possibly in early form. Accepted submissions in this category will be published in the main proceedings and will be presented as short talks.

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 22:06):

Presumably you can go without presenting a paper?

view this post on Zulip Kevin Buzzard (Mar 11 2018 at 22:06):

Then you get the best of both worlds

view this post on Zulip Patrick Massot (Mar 11 2018 at 22:06):

It's easier when you go from London to Oxford than from Canada to Oxford

view this post on Zulip Mario Carneiro (Mar 11 2018 at 22:13):

I'm aiming for ITP 2018, if all goes well I will be in Oxford this summer

view this post on Zulip Mario Carneiro (Mar 11 2018 at 22:13):

(to present the Matiyasevich proof)

view this post on Zulip Patrick Massot (Mar 11 2018 at 22:13):

nice

view this post on Zulip Andrew Ashworth (Mar 12 2018 at 00:21):

what's more interesting to me is that they've rolled up 9 conferences into one. just how many people attend these things in person?

view this post on Zulip Gabriel Ebner (Mar 12 2018 at 07:27):

I will (most likely) be in Oxford as well, though I haven't sent anything to ITP.

view this post on Zulip Kevin Buzzard (Mar 12 2018 at 07:33):

We tend to have specialised algebraic number theory conferences around once every 2 years, and there tend to be hundreds of us that go.

view this post on Zulip Kevin Buzzard (Mar 12 2018 at 07:34):

Is it the sort of thing where you can just not bother registering and then show up on the day and meet people and chat to them and gatecrash a few talks (like pretty much every pure maths conference would be)?

view this post on Zulip Kevin Buzzard (Mar 12 2018 at 07:35):

My partner goes to medical conference which cost $100s to register and you can't get past security without a badge

view this post on Zulip Kevin Buzzard (Mar 12 2018 at 07:35):

I go to maths conferences and the worst that can happen if you don't register is that you have to pay for your own lunch

view this post on Zulip Gabriel Ebner (Mar 12 2018 at 08:04):

In my experience, you need to register if you 1) present a paper, 2) want lunch, or 3) want a lanyard. I haven't seen strict badge controls so far.

view this post on Zulip Johannes Hölzl (Mar 12 2018 at 08:47):

ITP and CPP are the biggest theorem proving conferences. If you go through the proceedings of the last years you can find some interesting stuff. Also, in computer science, publishing at a conference usually counts as a regular publication. But this means the program committees are bigger, as people need to review the papers upfront. And of course, you can go there without presenting a paper.

view this post on Zulip Assia Mahboubi (Mar 14 2018 at 11:12):

@Patrick Massot , I wish I could be more positive but it would not be honest: I do not think that it would be reasonable in your case to go from Canada to Oxford specifically for that event (I hope that Jeremy is not reading...).
It will be very much a CS-style event with short talks meant to be teasers for the paper in the proceedings. As it is part this year of the Federated Logic Conference, it will take place in parallel with other even larger events, and people will possibly spend time rushing between the parallel sessions of a rather dense agenda... Usually, only a fraction of these talks are about formalized maths (as opposed for instance to program verification in general). But I have high expectations for Dan Grayson's invited talk. He will deliver a talk in memoriam of Vladimir Voevodsky but we hope that he will also speak about his own opinion about formalizing mathematics.

view this post on Zulip Assia Mahboubi (Mar 14 2018 at 11:20):

Or do most people just do nothing?

@Kevin Buzzard Again, it is very much a CS-style event... These people are reviewing the papers submitted for the proceedings of the conference. In the case of this conference, they had 2 months to read an average of 6 submitted papers. Each of this paper is at most 15 pages and in the case of ITP, papers are usually accompanied with code. So I find it quite demanding to serve on such a committee.

view this post on Zulip Patrick Massot (Mar 14 2018 at 11:44):

I'm not the one traveling from Canada, that was a comment about Kevin's answer to Simon (Simon is from Canada). I would be travelling from Paris.

view this post on Zulip Patrick Massot (Mar 14 2018 at 11:45):

I'll probably wait for the talk abstracts, but it seems I shouldn't be too optimistic

view this post on Zulip Patrick Massot (Mar 14 2018 at 11:45):

And now I have to teach finite fields


Last updated: May 14 2021 at 00:42 UTC