Profile

Cover photo
Geoffrey Irving
Works at Eddy Systems
Attended California Institute of Technology
187 followers|29,855 views
AboutPostsPhotosVideos

Stream

Geoffrey Irving

Shared publicly  - 
 
 
The link below is to a paper put out by the IMF that attempts to estimate the amount by which fossil fuels are subsidized. The answers are staggeringly large. The good news is that although quite a large fraction of the subsidy is as a result of not making them pay for the adverse effects of climate change, this is outweighed by the subsidy as a result of not making them pay for local damage, such as the costs associated with the effect of pollution on people's health.

This is in principle very good news indeed, because it means that it is in the interests of countries like China to cut down on fossil fuel subsidy even if they act unilaterally. So the seemingly intractable prisoner's-dilemma aspect of the problem may not be so bad after all. In the words of the report itself:


Most energy subsidies arise from the failure to adequately charge for the cost of domestic environmental damage—only about one-quarter of the total is from climate change—so unilateral reform of energy subsidies is mostly in countries’ own interests, although global coordination could strengthen such efforts.

The fiscal, environmental, and welfare impacts of energy subsidy reform are potentially enormous. Eliminating post-tax subsidies in 2015 could raise government revenue by $2.9 trillion (3.6 percent of global GDP), cut global CO2 emissions by more than 20 percent, and cut premature air pollution deaths by more than half. After allowing for the higher energy costs faced by consumers, this action would raise global economic welfare by $1.8 trillion (2.2 percent of global GDP).

It is sometimes said that to persuade climate-change deniers of the need to cut down on fossil fuels, one needs to present them with a positive vision of what the future would be like if we did so, rather than an avoiding-doom picture. Now, amazingly, it looks as though we have the means to do that. Maybe you don't believe in AGW, or believe that money spent combating it would be better spent directly combating poverty. But if the IMF is correct, then ending subsidies on fossil fuels will make us better off, so it will help us to alleviate poverty, whether or not you believe in the other benefits of reducing emissions.
6 comments on original post
3
Add a comment...

Geoffrey Irving

Shared publicly  - 
 
Continuing a worrisome trend.
Windows 10 hardware must support Secure Boot and won't have to let you turn it off.
2
Add a comment...

Geoffrey Irving

Shared publicly  - 
 
What, you don't check in your .Git/cOnFiG files?  https://github.com/blog/1938-vulnerability-announced-update-your-git-clients
1
Add a comment...

Geoffrey Irving

Shared publicly  - 
 
The next (old) step after injecting headers into HTTP packets.
Recently, Verizon was caught tampering with its customer's web requests to inject a tracking super-cookie. Another network-tampering threat to user safety has come to light from other providers: email encryption downgrade attacks.
1
Jed Brown's profile photo
 
I have observed this attack. It was common in France this summer. 

People talk about the protocol being broken and act like switching the port would fix the problem.  But the real problem is that servers either don't support TLS or have self-signed certificates.  If everyone had signed certs, we could configure our servers to make STARTTLS non-optional and to verify the certs.  As it is now, the best you can do is attempt STARTTLS and save info about the connection in logs.
Add a comment...

Geoffrey Irving

Shared publicly  - 
 
1
Add a comment...

Geoffrey Irving

Shared publicly  - 
 
 
If you care about open-source software, please read this carefully and consider the impact of the Dept. of Energy - one of the largest funders of open-source software in the world - publishes the following as an official statement.  This document is being submitted to Secretary Moniz and will presumably be read by Congressional staff.

"There has been very little open source that has made its way into broad use within the HPC commercial community where great emphasis is placed on serviceability and security. There is a better track record in data analytics recently with map/reduce as a notable example.
...
It should be noted that the most significant consumption of open source software is China and it is also the case that the Chinese are rare contributors to open source as well. Investments in open source or other policy actions to stimulate creation are likely to produce a disproportionate benefit accruing to the Chinese."

If you know any of the committee members responsible for this document (they are listed at the end), considering contacting them about this.
This report of the SEAB Task Force on High Performance Computing sets forth its findings and recommendations to date in three timely and important areas
1
Add a comment...
In his circles
202 people
Have him in circles
187 people
Robert Harris's profile photo
hassan Amghibech's profile photo
Lajosné Gergely's profile photo
Andrew Selle's profile photo
Chad Ritchie's profile photo
Piattini Bocaraton's profile photo
Shara Maikranz's profile photo
Chris Wojtan's profile photo
Judy Jou's profile photo

Geoffrey Irving

Shared publicly  - 
 
Demo video and reddit thread for my eddy project: autocorrect for Java
2
Add a comment...

Geoffrey Irving

Shared publicly  - 
 
It would be nice to be better than China here.
Stringent regulations, including a requirement to share secret codes, are another form of economic protectionism, Western technology companies say.
1
Sean McDirmid's profile photoGeoffrey Irving's profile photo
12 comments
 
Alas!
Add a comment...

Geoffrey Irving

Shared publicly  - 
 
Concept demo for eddy, our interactive programming startup.
Write less code, get more done. eddy is an interactive programming system designed to make life easier for programmers.
4
Matthew Knepley's profile photoGeoffrey Irving's profile photo
2 comments
 
The first version will be almost entirely type based, so that's difficult. Beyond the short term, we believe the inference could be made nearly as good using imperfect, heuristic types, but the lack of static language types will likely make the failure case less pleasant. That is, when eddy fails to guess what you mean, it would usually be a type error in Java and a confusing runtime error in Python.
Add a comment...

Geoffrey Irving

Shared publicly  - 
 
A proposal for an ever so slightly less unsafe language.
[This post is jointly authored by Pascal Cuoq, Matthew Flatt, and John Regehr.] In this post, we will assume that you are comfortable with the material in all three parts of John's undefined behavior writeup and also with all three parts of Chris Lattner's writeup about undefined behavior.
1
Geoffrey Irving's profile photo
 
Isn't it a tiny bit of everything you ever wanted?
Add a comment...

Geoffrey Irving

Shared publicly  - 
 
Anyone with SMT solver experience (satisfiability modulo theory)?  In particular, do any of the open source versions hold up against Z3?
1
Geoffrey Irving's profile photoMathieu Desbrun's profile photo
3 comments
 
VeriT is slow, but good!
Add a comment...

Geoffrey Irving

Shared publicly  - 
 
 
FLYSPECK has finished!

The Flyspeck project [0], aimed at finding a formal proof of the Kepler conjecture [1] has reached its goal! I can't top the description in the announcement below, so I will only add a few words. This is a long journey from the 1998 first proof, the by-hand parts of which appeared (seven years after submission!) in the Annals of Mathematics [2], but about which referees were only willing to say they were "99% confident" that the proof was correct, due to the complex computer-assisted calculations. Note that there is a 500MB zip file containing everything related to the linear programming problem code maintained on the Annals website.

The announcement email from Tom Hales is below. Worth watching is his lecture at the Institut Henri Poincaré [3] from earlier this year.

[0] https://code.google.com/p/flyspeck/
[1] http://en.wikipedia.org/wiki/Kepler_conjecture
[2] http://dx.doi.org/10.4007/annals.2005.162.1065
[3] 3 - Kick-off afternoon : Thomas Hales, Formalizing the proof of the Kepler Conjecture

#mathematics   #scienceeveryday  

==========

---------- Forwarded message ----------
From:  <HALES@pitt.edu>
Date: Sun, Aug 10, 2014 at 4:26 PM
Subject: Flyspeck project completion
To: Thomas Hales <hales@pitt.edu>



We are pleased to announce the completion of the Flyspeck project,
which has constructed a formal proof of the Kepler conjecture.  The
Kepler conjecture asserts that no packing of congruent balls in
Euclidean 3-space has density greater than the face-centered cubic
packing.  It is the oldest problem in discrete geometry.  The proof of
the Kepler conjecture was first obtained by Ferguson and Hales in
1998.  The proof relies on about 300 pages of text and on a large
number of computer calculations.

The formalization project covers both the text portion of the proof
and the computer calculations.  The blueprint for the project appears
in the book "Dense Sphere Packings," published by Cambridge University
Press.  The formal proof takes the same general approach as the
original proof, with modifications in the geometric partition of space
that have been suggested by Marchal.

----

A formal proof is a mathematical proof that has been checked by
computer from the foundational axioms of mathematics and primitive
inference rules.  A formal proof provides a much higher degree of
certification than traditional standards of rigor and peer review by
referees.

The formal proof has been constructed in a combination of the Isabelle
and HOL Light formal proof assistants.

The Isabelle portion of the formalization, which was carried out by
Bauer and Nipkow, classifies all tame graphs.  This enumerates the
combinatorial structures of potential counterexamples to the Kepler
conjecture.

This classification theorem has been translated directly by hand into a
corresponding term `import_tame_classification` in the HOL Light proof
assistant.  At a conceptual level, the classification theorem could be
formulated as a large SAT problem, and SAT problems pass easily from
one proof assistant to another.

The rest of the formalization has been carried out in HOL Light,
producing a formal theorem

|- import_tame_classification /\ the_nonlinear_inequalities
                              ==> the_kepler_conjecture

where `the_kepler_conjecture` is defined as the following term

`(!V. packing V
            ==> (?c. !r. &1 <= r
                         ==> &(CARD(V INTER ball(vec 0,r))) <=
                             pi * r pow 3 / sqrt(&18) + c * r pow 2))`

In standard mathematical language, this states that for every packing
V (which is identified with the set of centers of balls of radius 1),
there exists a constant c controlling the error term, such that for
every radius r that is at least 1, the number of ball centers inside a
spherical container of radius r is at most pi * r^3 / sqrt(18), plus
an error term of smaller order.  As r tends to infinity, this gives
the density bound pi / sqrt(18) = 0.74+, which is the density of the
face-centered-cubic packing.

The term `the_nonlinear_inequalities` is defined as a conjection of
several hundred nonlinear inequalities.  The domains of these
inequalities have been partitioned to create more than 23,000
inequalities.  The verification of all nonlinear inequalities in HOL
Light on the Microsoft Azure cloud took approximately 5000
processor-hours. Almost all verifications were made in parallel with
32 cores, hence the real time is about 5000 / 32 = 156.25
hours. Nonlinear inequalities were verified with compiled versions of
HOL Light and the verification tool developed in Solovyev's 2012
thesis.

To check that no pieces were overlooked in the distribution of
inequalities to various cores, the pieces have been reassembled in a
specially modified version of HOL Light that allows the import of
theorems from other sessions of HOL light.  In that version, we obtain
a formal proof of the theorem

|- the_nonlinear_inequalities

----

The code for the project is available for download from
http://afp.sourceforge.net/devel-entries/Flyspeck-Tame.shtml (Isabelle
tame graphs)
https://code.google.com/p/flyspeck/ (HOL Light Flyspeck project).

There have been many contributors to the project as indicated in the
credits below.  Many of them will be co-authors of the published
account of the formal proof.

Sincerely,

Thomas Hales, Alexey Solovyev, Hoang Le Truong,
and the Flyspeck Team
August 10, 2014

----

CREDITS

Project Director: Thomas Hales

Project Managers: Ta Thi Hoai An, Mark Adams

HOL Light libraries and support: John Harrison,

Isabelle Tame Graph Classification: Gertrud Bauer, Tobias Nipkow,

Chief Programmer: Alexey Solovyev,
-  Nonlinear inequalities: Victor Magron, Sean McLaughlin,  Roland Zumkeller,
-  Linear Programming: Steven Obua,
-  Microsoft Azure Cloud support: Daron Green,  Joe Pleso, Dan Synek,
Wenming Ye,

Chief Formalizer: Hoang Le Truong,
-  Text formalization: Jason Rute, Dang Tat Dat, Nguyen Tat Thang, Nguyen
Quang Truong,
        Tran Nam Trung, Trieu Thi Diep, Vu Khac Ky, Vuong Anh Quyen,

Student Projects: Catalin Anghel,  Matthew Wampler-Doty, Nicholas Volker,
        Nguyen Duc Tam, Nguyen Duc Thinh,  Vu Quang Thanh,
Proof Automation: Cezary Kaliszyk,  Josef Urban,
Editing: Erin Susick, Laurel Martin, Mary Johnston,
External Advisors and Design: Freek Wiedijk, Georges Gonthier, Jeremy
Avigad, Christian Marchal,

Institutional Support: NSF, Microsoft Azure Research, William Benter
Foundation,
              University of Pittsburgh, Radboud University,
              Institute of Math (VAST), VIASM.
3
1
Matthew Knepley's profile photo
Add a comment...
People
In his circles
202 people
Have him in circles
187 people
Robert Harris's profile photo
hassan Amghibech's profile photo
Lajosné Gergely's profile photo
Andrew Selle's profile photo
Chad Ritchie's profile photo
Piattini Bocaraton's profile photo
Shara Maikranz's profile photo
Chris Wojtan's profile photo
Judy Jou's profile photo
Education
  • California Institute of Technology
    Mathematics and Computer Science, 1999 - 2003
  • Stanford University
    Computer Science, 2003 - 2007
Links
Other profiles
Work
Employment
  • Eddy Systems
    Founder, 2014 - present
  • Otherlab
    Research Scientist, 2011 - 2014
Basic Information
Gender
Male