Zhong Shao, Yale, The Flint Group, here. Look at Shao’s links page, here. Between these folks and Appel at Ptown – seems like something is going to happen. I would like it if there was some formal numerical error bounds that could come out of these proof systems. Just for expression evaluation to start would be fine. There are countless Java programming folks coercing double arithmetic to BigDecimal because someone told them that round off for currency is some kind of rocket science project in precision loss.
The FLINT group at Yale aims to develop a novel and practical programming infrastructure for constructing large-scale certified systems software. By combining recent new advances in programming languages, formal semantics, certified operating systems, program verification, proof assistants and automation, language-based secrurity, and certifying compilers, we hope to attack the following research questions:
- what OS kernel structures can offer the best support for extensibility, security, and resilience?
- what program logics and semantic models can best capture these abstractions?
- what are the right programming languages and environments for developing such certified kernel? and
- how to build new automation facilities to make certified software really scale?
Khachiyan’s “rocket” had actually left the hangar ten months before, in a January 1979 Doklady Akademii Nauk paper whose title translates into English as, “A polynomial algorithm for linear programming.” As recounted by Berkeley’s Eugene Lawler, it was sighted at a May 1979 meeting Lawler attended in Oberwohlfach, and after Peter Gács and László Lovász supplied proofs missing in the paper, it was pronounced correct at a conference in Montreal. The discovery was picked up in October by Science News, and then by the magazine Science. An allusion by the latter to the NP-complete Traveling Salesman problem was moved to the headline of a Nov. 4 story in England’s Guardian newspaper, and reflected three days later in the New York Times’s front-page screamer, “A Soviet Discovery Rocks World of Mathematics.”
Our point is not to say that linear programming being in was a surprise. To those who knew the reality behind the headlines, it wasn’t. As Lawler relates, the great George Dantzig had tried to set Times reporter Malcolm Browne straight on this and points related to what LP’s can and (ostensibly) cannot solve. The simplex algorithm already solved the vast majority of LP cases in expected time, so there was no feeling of practical intractability. Rather our point draws on something perhaps less widely known and appreciated: that Khachiyan’s ideas extend to solve a much wider class than linear programs, called semi-definite programs or SDP’s. Thus it can be said to show that a complexity class defined by reductions to these programs equals .