Sputnik, the very first artificial satellite, was launched from Kazakhstan almost a half-century ago. This unexpected event sent shockwaves through the US’s math-science public education establishment. George Hacken was in high school, and was lucky enough to pass the exam for a Sputnik-inspired extracurricular IBM/Joe Berg Foundation course in discrete math (whose textbook was Kemeny, Snell, and Thomson’s Finite mathematics). As must be true of many CR readers, he never got over it, that is, over logic and discrete math.

He majored in physics (AB and PhD) at Columbia, where he stayed on as a researcher until 1976, and enjoyed with fellow students and post-docs the reflected glory of his thesis sponsor’s 1975 Nobel Prize. (Professor James Rainwater had him pegged from the beginning as a computer geek, and George did his best to be useful as a discrete math, computational complement of his awesome physico-geometric intuition.)

His first program (1962, Fortran II, IBM 1620) was a multidimensional constrained minimization problem; it was a lesson par excellence in the downright practicality of trying to “get it right the first time” — a personal augury of formal methods. The year 1976 saw another defining moment: he serendipitously came upon E.W. Dijkstra’s A discipline of programming. He had, by then, written approximately 5,000 programs, the later ones for a special, scientific model of the IBM 360, the 44, and all in connection with physics research. Dijkstra’s masterpiece changed his life, as it changed the lives of many others.

Career progression, not necessarily logical but certainly chronological, saw computing venues in telephone company rate-structure calculations; computations of credit card delinquency risk; flight simulation; factory-automation and sawmill process control; radiation-dosimetry safety-critical database work; and railroad-car brake control. These projects were followed by a 15-year aerospace defense stint at Singer-Kearfott/Plessey/GEC-Marconi, where embedded computers effected guidance, navigation, and control, and command, control, communications, and intelligence. There was also a concurrent activity as adjunct professor of computer science at William Paterson University.

Great respect for the expertise of the late Austin J. Maher (his boss and mentor at Singer-Kearfott) led to Hacken’s minimal resistance in joining Maher and the Council of Defense And Space Industries (CODSIA) government industry group in the collective creation of DoD-Std-2167, Defense System Software Development, which is fairly characterized as one of the precursors of the Capability-Maturity Model (CMM). This was a most natural segue, seven years later, into the job as CMM process lead in the company’s GEC-Marconi incarnation.

Seven years ago, Hacken started his current job as Senior Director of Vital [a.k.a. Safety-Critical] Systems Integrity at MTA/New York City Transit, where formal methods are being applied in the design, certification, and implementation of processor-based train control technologies. A most rewarding part of his job is the creation and execution of an in-house safety-critical systems design and certification course. He is, in addition to being an ACM and IEEE member, greatly informed by membership in the New York Academy of Sciences, Sigma Xi, and the American Mathematical Society.

By the way, he was born in Kazakhstan, but that’s another story.

Formal verification of control system software Garoche P., PRINCETON UNIVERSITY PRESS, Princeton, NJ, 2019. 224 pp. Type: Book (978-0-691181-30-1) This outstanding work manages to deal with key topics, many of which are highly advanced, while also being encyclopedic (in a good sense) within a mere 200 pages. In spite of its advanced nature, all levels of reader will be informed or well direc...

May 10 2021

Introduction to logic programming Genesereth M., Chaudhri V., Morgan & Claypool, San Rafael, CA, 2020. 199 pp. Type: Book (978-0-374279-75-2) Some time ago, our (then) teenage daughter used to exclaim, “Get with the ’80s!” whenever my wife and I imposed an eminently reasonable restriction. The very loose, perhaps reverse analogy here is that a computing pro...

Dec 15 2020

Reverse mathematics: proofs from the inside out Stillwell J., PRINCETON UNIVERSITY PRESS, Princeton, NJ, 2018. 200 pp. Type: Book Reverse mathematics “seeks the axioms needed to prove given theorems.” The work of Emil Post and Kurt Gödel, in the 1920s and 1930s, permanently dashed the hope that axiom systems could formally generate all theorems for natural n...

Nov 23 2020

Essential logic for computer science Page R., Gamboa R., The MIT Press, Cambridge, MA, 2018. 304 pp. Type: Book (978-0-262039-18-5) The “for computer science” part of this excellent book’s title initially gave me pause, as it connoted for me a possible compromise of the “logic” part. As a matter of fact, the very opposite is the case here. The boo...

Oct 2 2020

Formal methods: an appetizer Nielson F., Nielson H., Springer International Publishing, New York, NY, 2019. 162 pp. Type: Book (978-3-030051-55-6) I’ve occasionally been intimidated into ordering an appetizer as the main course, but have rarely regretted it thanks to the presence of “gourmet” friends. This is an excellent, ultra-elegant, and rigorous book. Its 160 printed p...

Apr 23 2020

On the impact of programming languages on code quality: a reproduction study Berger E., Hollenbeck C., Maj P., Vitek O., Vitek J. ACM Transactions on Programming Languages and Systems 41(4): 1-24, 2019. Type: Article E. W. Dijkstra’s classic A discipline of programming [1] has rightly achieved the sort of permanent validity that mathematician G. H. Hardy spoke of in his famous A mathematician’s apology [2]. Dijkstra’s preface ex...

Nov 21 2019

Bits and bugs: a scientific and historical review of software failures in computational science Huckle T., Neckel T., Society for Industrial and Applied Mathematics, Philadelphia, PA, 2019. 251 pp. Type: Book (978-1-611975-55-0) Niels Bohr, in confronting the subtleties and paradoxes of quantum theory, said to one of his many famous students and acolytes, “These issues are so serious that one can only joke about them” [1]. The vernacular main title of this exc...

Nov 20 2019

Efficiency through uncertainty: scalable formal synthesis for stochastic hybrid systems Cauchi N., Laurenti L., Lahijanian M., Abate A., Kwiatkowska M., Cardelli L. HSCC 2019 (Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, Montreal, Canada, Apr 16-18, 2019) 240-251, 2019. Type: Proceedings Hybrid systems are those “with both continuous dynamics and discrete logic” [1]. The discrete logic serves to label or parametrize (my terms) states; state-specific continuous dynamics, modeled largely if not exclusively by differentia...

Jul 12 2019

An open door to number theory Campbell D., AMERICAN MATHEMATICAL SOCIETY, Washington, DC, 2018. 283 pp. Type: Book (978-1-470443-48-1) In 1993, my daughter showed me the New York Times article that announced Andrew Wiles’s 100-plus-page proof (to be successfully corrected two years later) of Fermat’s last theorem (FLT) [1]. Wiles’s “20th-centuryR...

Feb 19 2019

A generalized digraph model for expressing dependencies Fradet P., Guo X., Monin J., Quinton S. RTNS 2018 (Proceedings of the 26th International Conference on Real-Time Networks and Systems, Chasseneuil-du-Poitou, France, Oct 10-12, 2018) 72-82, 2018. Type: Proceedings The authors characterize this paper as a work in progress in computer assisted verification (CAV) of task-scheduling models. Directed graph (digraph) models are expressive; however, as the authors point out, they are limited with respect to “...