Тоні Гоар

Сер Чарлз Ентоні Річард Гоар (англ. Charles Antony Richard Hoare або Tony Hoare або C.A.R. Hoare, народився 11 січня 1934, Коломбо, Цейлон, Британська імперія, сьогодні Шрі-Ланка) — англійський вчений, що працює в галузі інформатики та обчислювальної техніки. Найбільш відомий як розробник алгоритму «швидкого сортування» (англ. «quick sort»).

Чарлз Ентоні Річард Гоар
Charles Antony Richard Hoare
Народився 11 січня 1934(1934-01-11) (88 років)
Коломбо, Цейлон, Британська імперія, сьогодні Шрі-Ланка
Місце проживання Кембридж
Країна Велика Британія
Діяльність інформатик, інженер, програміст, письменник, викладач університету
Alma mater Оксфордський університет, МГУ
Галузь інформатика
Заклад Microsoft, Університет Оксфорда і Королівський університет Белфаста
Аспіранти, докторанти Білл Роско, Cliff Jonesd, Augusto Sampaiod, William James Stewartd[1], Stephen D. Brookesd[1], David Andrew Naumannd[1], Andrew Philip Blackd[1], Peter Lauerd[1], Jeremy Jacobd[1], Masud Malikd[1], John Elderd[1], Jim (Wolfgang) Kaubischd[1], Richard Kennawayd[1], T. Yung Kongd[1], Geraint Jonesd[1], Christopher Dollind[1], Alex Terueld[1], Bryan Toddd[1], Stephen Paged[1], Clare Martind[1], Ken Woodd[1], Stephen Briend[1] і Paul Rudind[1]
Членство Лондонське королівське товариство, Національна академія деї Лінчеї, Європейська академія[2], Баварська академія наук, Національна академія наук США і UK Computing Research Committeed[3]
Відомий завдяки:

алгоритм швидкого сортування

Логіка Гоара
Батько Henry Samuel Malortie Hoared[4]
Мати Marjorie Francis Villiersd[4]
Нагороди Премія Тюрінга
Особ. сторінка cs.ox.ac.uk/people/tony.hoare/
 Тоні Гоар у Вікісховищі

Інші відомі результати його праці: мова Z специфікацій та паралельна модель взаємодії послідовних процесів (CSP, Communicating Sequential Processes). Серед його досягнень — розробка логіки Гоара, наукової основи для конструювання коректних програм, яка використовується для визначення та розробки мов програмування. Гоар написав низку праць зі створення специфікацій, проектування, реалізації та супроводу програм, що висвітлюють важливість наукових досліджень для збільшення продуктивності комп'ютерів та збільшення надійності програмного забезпечення.

Біографія

Народився в Коломбо в Шрі-Ланці. Отримав ступінь бакалавра з класичних мов в Оксфордському університеті у 1956 році. Проходив службу у ВМС Великої Британії у 1956—1958 роках. Вивчивши російську мову, навчався комп'ютерного перекладу під керівництвом А. Н. Колмогорова в Московському Державному Університеті. У 1960 він залишив СРСР через політичну кризу (знищення розвідувального літака U-2) та почав працювати в невеликій компанії з виробництва комп'ютерів Elliot Brothers, де працював над реалізацією мови програмування ALGOL60. Тоді ж розпочав займатися розробкою алгоритмів.

1968 року Гоар став професором інформатики та обчислювальної техніки в Королівському Університеті Белфаста

1977 повернувся в Оксфорд як професор з обчислювальної техніки, щоб взяти під керівництво дослідницьку групу Programming Research Group, до задач якої входили зміцнення промислових, академічних та державних структур, що працюють в індустрії інформаційних технологій. Тема його досліджень в Оксфорді: коректність програмних специфікацій, проектування та розробка критичних та некритичних систем.

1999 року вийшов на пенсію у званні почесного професора та перейшов на посаду дослідника в Microsoft Research в Кембриджі, де й працює сьогодні.

1980 Гоар отримав Премію Тюринґа за «видатні досягнення у визначенні та дизайні мов програмування».[5]

У 2000 році Чарлз Ентоні Річард Гоар був відзначений лицарським званням; того ж року — Премією Кіото у галузі освіти та комп'ютерних наук.

У 2011 отримав Медаль Джона фон Неймана.

Наукові досягнення

Зізнання

Виступаючи на конференції QCon London в 2009, він вибачився за винайдення нульового вказівника:[6]

Я називаю це своєю помилкою на мільярд доларів. Це було винайдення нульового вказівника в 1965. В той час я розробляв першу вичерпну систему типів для посилань в об'єктно-орієнтованій мові (ALGOL W). На меті в мене було зробити, щоб всі використання посилань мають бути цілком безпечні, з перевіркою, що виконується компілятором автоматично. Але я не зміг втриматись від спокуси додати нульовий вказівник, просто тому, що його було легко реалізувати. Це призвело до незліченних помилок, вразливостей і відмов систем, які напевне спричинили мільярдні збитки й шкоду за останні сорок років.

Оригінальний текст (англ.)
I call it my billion-dollar mistake. It was the invention of the null reference in 1965. At that time, I was designing the first comprehensive type system for references in an object oriented language (ALGOL W). My goal was to ensure that all use of references should be absolutely safe, with checking performed automatically by the compiler. But I couldn't resist the temptation to put in a null reference, simply because it was so easy to implement. This has led to innumerable errors, vulnerabilities, and system crashes, which have probably caused a billion dollars of pain and damage in the last forty years.

Протягом багатьох років під його керівництвом відділ в Оксфорді працював над мовами формальної специфікації, такими як CSP та Z. Але індустрія програмного забезпечення не підхопила цю ідею як очікувалося, тому в 1995 Гоар переглянув початкові припущення:[7]

Десятиліття тому, дослідники формальних методів (і я серед них помилявся найбільше) передбачали, що світ програмування з вдячністю прийме будь-яку допомогу, яку надасть формалізація у розв'язанні проблем надійності, яка виникає, коли програми стають великими й більш критичними щодо безпеки. Зараз програми стали дуже великими й дуже критичними - далеко за масштабами, з якими можна комфортно працювати за допомогою формальних методів. Було багато проблем і невдач, але їх завжди приписували недостатньому аналізу вимог чи недостатньому контролю з боку менеджменту. Виявилось, що світ ще не достатньо страждає від проблем, які початково намагалися вирішити наші дослідження.

Оригінальний текст (англ.)
Ten years ago, researchers into formal methods (and I was the most mistaken among them) predicted that the programming world would embrace with gratitude every assistance promised by formalisation to solve the problems of reliability that arise when programs get large and more safety-critical. Programs have now got very large and very critical – well beyond the scale which can be comfortably tackled by formal methods. There have been many problems and failures, but these have nearly always been attributable to inadequate analysis of requirements or inadequate management control. It has turned out that the world just does not suffer significantly from the kind of problem that our research was originally intended to solve.

Примітки
  1. Математична генеалогія — 1997.
  2. https://www.ae-info.org/ae/User/Hoare_Charles
  3. https://www.theiet.org/impact-society/thought-leadership/expert-panels/uk-computing-research-committee-ukcrc/members-of-ukcrc/ukcrc-members/
  4. Lundy D. R. The Peerage
  5. http://awards.acm.org/citation.cfm?id=4622167&srt=year&year=1980&aw=140&ao=AMTURING Архівовано 1 липня 2012 у Archive.is ACM Award Citation / C.Antony R. Hoare
  6. Hoare, Tony (25 серпня 2009). Null References: The Billion Dollar Mistake. InfoQ.com.
  7. Hoare, C. A. R. (1996). Unification of Theories: A Challenge for Computing Science. Selected papers from the 11th Workshop on Specification of Abstract Data Types Joint with the 8th COMPASS Workshop on Recent Trends in Data Type Specification. Springer-Verlag. с. 49–57. ISBN 3-540-61629-2.

Бібліографія
  • C. A. R. Hoare, Communicating Sequential Processes. Prentice Hall International Series in Computer Science, 1985. ISBN 0-13-153271-5 hardback or ISBN 0-13-153289-8 paperback.
  • C. A. R. Hoare and M. J. C. Gordon, Mechanised Reasoning and Hardware Design. Prentice Hall International Series in Computer Science, 1992. ISBN 0-13-572405-8.
  • C. A. R. Hoare and He Jifeng, Unifying Theories of Programming. Prentice Hall International Series in Computer Science, 1998. ISBN 0-13-458761-8.

Посилання


This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.