Tony Hoare - Tony Hoare
Monsieur
Tony Hoare
| |
---|---|
Née |
Charles Antoine Richard Hoare
11 janvier 1934 |
Autres noms | VOITURE Hoare |
mère nourricière | |
Connu pour | |
Récompenses | |
Carrière scientifique | |
Des champs | L'informatique |
Établissements | |
Doctorants | |
Site Internet | www |
Sir Charles Antony Richard Hoare FRS FREng (né le 11 janvier 1934) est un informaticien britannique .
Tony Hoare a développé l' algorithme de tri rapide en 1959-1960. Il a également développé la logique de Hoare pour vérifier l'exactitude du programme, et le langage formel communiquant des processus séquentiels (CSP) pour spécifier les interactions des processus concurrents (y compris le problème des philosophes de la restauration ) et l'inspiration pour le langage de programmation occam .
Hoare a été élu membre de la National Academy of Engineering en 2006 pour ses contributions fondamentales à l'informatique dans les domaines des algorithmes, des systèmes d'exploitation et des langages de programmation.
Éducation et jeunesse
Tony Hoare est né à Colombo , Ceylan (aujourd'hui Sri Lanka ) de parents britanniques ; son père était fonctionnaire colonial et sa mère était la fille d'un planteur de thé. Hoare a fait ses études en Angleterre à la Dragon School d' Oxford et à la King's School de Canterbury . Il a ensuite étudié les classiques et la philosophie ("Greats") au Merton College d'Oxford . Après avoir obtenu son diplôme en 1956, il a effectué 18 mois de service national dans la Royal Navy , où il a appris le russe. Il retourna à l' Université d'Oxford en 1958 pour préparer un certificat de troisième cycle en statistiques , et c'est là qu'il commença la programmation informatique , après avoir appris l' Autocode sur le Ferranti Mercury par Leslie Fox . Il est ensuite allé à l'Université d'État de Moscou en tant qu'étudiant d'échange du British Council , où il a étudié la traduction automatique avec Andrey Kolmogorov .
Recherche et carrière
En 1960, Hoare a quitté l' Union soviétique et a commencé à travailler chez Elliott Brothers Ltd , une petite entreprise de fabrication d'ordinateurs située à Londres. Là, il a implémenté le langage ALGOL 60 et a commencé à développer des algorithmes majeurs .
Il a participé à l'élaboration de normes internationales en programmation et en informatique, en tant que membre du groupe de travail 2.1 de la Fédération internationale pour le traitement de l'information (IFIP) sur les langages algorithmiques et les calculs, qui a spécifié , maintient et prend en charge les langages ALGOL 60 et ALGOL 68 .
Il est devenu professeur d' informatique à l' Université Queen's de Belfast en 1968 et, en 1977, il est retourné à Oxford en tant que professeur d'informatique pour diriger le groupe de recherche sur la programmation au laboratoire d'informatique de l'Université d'Oxford (aujourd'hui Département d'informatique, Université d'Oxford ). , suite au décès de Christopher Strachey . Il y est maintenant professeur émérite et chercheur principal à Microsoft Research à Cambridge , en Angleterre.
Les travaux les plus importants de Hoare ont porté sur les domaines suivants : son algorithme de tri et de sélection ( Quicksort et Quickselect ), la logique de Hoare , le langage formel communiquant des processus séquentiels (CSP) utilisé pour spécifier les interactions entre les processus concurrents , la structuration des systèmes d'exploitation informatiques à l'aide du moniteur concept, et la spécification axiomatique des langages de programmation .
Excuses et rétractations
S'exprimant lors d'une conférence sur les logiciels en 2009, Tony Hoare s'est excusé d'avoir inventé la référence nulle :
J'appelle ça mon erreur d'un milliard de dollars. C'était l'invention de la référence nulle en 1965. A cette époque, je concevais le premier système de types complet pour les références dans un langage orienté objet ( ALGOL W ). Mon objectif était de m'assurer que toute utilisation de références devait être absolument sûre, avec une vérification effectuée automatiquement par le compilateur. Mais je n'ai pas pu résister à la tentation de mettre une référence nulle, simplement parce que c'était si facile à mettre en œuvre. Cela a conduit à d'innombrables erreurs, vulnérabilités et plantages du système, qui ont probablement causé un milliard de dollars de souffrances et de dommages au cours des quarante dernières années.
Pendant de nombreuses années, sous sa direction, le département d'Oxford de Hoare a travaillé sur des langages de spécification formels tels que CSP et Z . Ceux-ci n'ont pas atteint l'adoption attendue par l'industrie, et en 1995 Hoare a été amené à réfléchir sur les hypothèses initiales :
Il y a dix ans, des chercheurs en méthodes formelles (et je me suis trompé le plus d'entre eux) ont prédit que le monde de la programmation accepterait avec gratitude toute aide promise par la formalisation pour résoudre les problèmes de fiabilité qui se posent lorsque les programmes deviennent volumineux et plus critiques pour la sécurité. Les programmes sont maintenant devenus très vastes et très critiques – bien au-delà de l'échelle qui peut être facilement abordée par des méthodes formelles. Il y a eu de nombreux problèmes et échecs, mais ceux-ci ont presque toujours été attribuables à une analyse inadéquate des besoins ou à un contrôle de gestion inadéquat. Il s'est avéré que le monde ne souffre tout simplement pas de manière significative du genre de problème que notre recherche était initialement destinée à résoudre.
Livres
- Dahl, O.-J. ; Dijkstra, EW ; Hoare, RCA (1972). Programmation structurée . Presse Académique . ISBN 978-0-12-200550-3. OCLC 23937947 .
- CAR Hoare (1985). Communiquer des processus séquentiels . Prentice Hall International Series en informatique. ISBN 978-0131532717 (relié) ou ISBN 978-0131532892 (broché). (Disponible en ligne sur http://www.usingcsp.com/ au format PDF.)
- Hoare, RCA ; Gordon, MJC (1992). Raisonnement mécanisé et conception de matériel . Prentice Hall International Series en informatique. ISBN 978-0-13-572405-7. OCLC 25712842 .
- Hoare, RCA ; Lui, Jifeng (1998). Théories unificatrices de la programmation . Prentice Hall International Series en informatique. ISBN 978-0-13-458761-5. OCLC 38199961 .
Personnel
En 1962, Hoare a épousé Jill Pym, membre de son équipe de recherche.
Prix et distinctions
- Membre distingué de la British Computer Society (1978)
- Prix Turing pour « contributions fondamentales à la définition et à la conception de langages de programmation ». Le prix lui a été remis lors de la conférence annuelle de l'ACM à Nashville, Tennessee , le 27 octobre 1980, par Walter Carlson, président du comité des prix. Une transcription du discours de Hoare a été publiée dans Communications of the ACM .
- Prix commémoratif Harry H. Goode (1981)
- Membre de la Royal Society (1982)
- Doctorat honorifique en sciences de la Queen's University Belfast (1987)
- Doctorat honorifique en sciences, de l' Université de Bath (1993)
- Membre honoraire, Kellogg College, Oxford (1998)
- Chevalier pour services rendus à l'éducation et à l' informatique (2000)
- Prix de Kyoto pour la science de l' information (2000)
- Membre de la Royal Academy of Engineering (2005)
- Membre de l' Académie nationale d'ingénierie (2006)
- Computer History Museum (CHM) à Mountain View, California Fellow of the Museum "pour le développement de l' algorithme Quicksort et pour des contributions permanentes à la théorie des langages de programmation " (2006)
- Doctorat honorifique de l' Université Heriot-Watt (2007)
- Doctorat honorifique en sciences du Département d'informatique de l' Université d'économie et de commerce d'Athènes (AUEB) (2007)
- Prix Friedrich L. Bauer, Université technique de Munich (2007)
- Prix SIGPLAN pour la réalisation des langages de programmation (2011)
- Médaille IEEE John von Neumann (2011)
- Doctorat honorifique, Université de Varsovie (2012)
- Doctorat honorifique, Université Complutense de Madrid (2013)
Les références
Cet article incorpore du texte disponible sous la licence CC BY 4.0 .