Tôn vinh dấu ấn của Tony Hoare về khoa học máy tính

Tony Hoare tại trường hè LASER, tháng 9 năm 2007
(Tất cả hình ảnh trong bài viết này là của tác giả)

Nếu chúng chỉ bao gồm một trong những thành tựu lớn của Tony Hoare thì nhiều sự nghiệp khoa học cũng đã được coi là đủ danh giá. Ông có một danh sách dài mà tôi sẽ cố gắng tóm tắt, không giả vờ là gần đến mức đầy đủ, nhân dịp đau buồn ông qua đời vào tuần trước ở tuổi 92. (Lưu ý: văn bản được đưa ra ở đây là bản nháp đầu tiên. Tôi sẽ hoàn thiện nó trong những ngày tới.)

Tôi sẽ nói về tính cách của C.A.R. Hoare, gần đây hơn là Giáo sư Ngài Tony Hoare (tên viết tắt của Charles Antony Richard nhưng ông luôn được biết đến với cái tên Tony) ở phần sau của bài viết này. Tuy nhiên, tôi nên lưu ý rằng đối với những ai không quen thuộc với văn bản của ông, “đóng góp của Hoare” cũng bao hàm một phong cách không thể nhầm lẫn. Trong bài giảng Turing [1], ông đã tuyên bố rõ ràng rằng đối với ông không có ranh giới rõ ràng giữa nghiên cứu và viết lách, và điều đó cho thấy. Ví dụ: đây là lời giải thích của anh ấy về quy tắc (sâu sắc) mà anh ấy đã đưa ra cho tiên đề đệ quy [2] ( “hồi quy vô hạn” sẽ là một chu kỳ vô tận dường như sẽ xảy ra sau đó đối với một người không thành thạo đệ quy, từ lệnh gọi đến một thủ tục xuất hiện trong phần thân của thủ tục đó):

Giải pháp cho sự hồi quy vô hạn rất đơn giản và ấn tượng: cho phép sử dụng kết luận mong muốn làm giả thuyết trong việc chứng minh chính cơ thể đó. Do đó, chúng tôi được phép chứng minh rằng phần thân thủ tục sở hữu một thuộc tính, trên giả định rằng mọi lệnh gọi đệ quy đều sở hữu thuộc tính đó và sau đó khẳng định một cách phân loại rằng mọi lệnh gọi, đệ quy hay cách khác, đều có thuộc tính đó. Giả định này về những gì chúng tôi muốn chứng minh trước khi bắt tay vào chứng minh giải thích rõ về hào quang kỳ diệu trong phần giới thiệu đầu tiên của lập trình viên về lập trình đệ quy.

Còn ai viết như thế này nữa? Phong cách là đặc điểm nổi bật trong tác phẩm của Hoare, không chỉ là phong cách viết mà còn là phong cách khoa học, luôn trang nhã và tập trung vào những gì thực sự quan trọng.

Đối với nhiều người, Hoare xuất hiện với tư cách là một giáo sư khoa học máy tính tinh túy và có thể đã nuôi dưỡng hình ảnh này (tôi không nhớ mình đã từng nhìn thấy ông ấy không đeo cà vạt hay có bất kỳ bức ảnh nào như vậy, và việc không mặc vest trên chiếc thuyền phía trên là một ngoại lệ); nhưng ấn tượng này một phần là sai lệch. Ông bắt đầu sự nghiệp của mình với tư cách là một lập trình viên và nhà quản lý trong ngành, một trải nghiệm được ông kể lại trong bài giảng Giải thưởng Turing [1]. Nền tảng học vấn của ông thật khác thường: ông được đào tạo về kinh điển tại Oxford. Một số công trình được đánh giá dưới đây của anh ấy có chiều sâu về toán học và logic và người ta thắc mắc làm thế nào anh ấy học được tài liệu đó. Ông không có bằng tiến sĩ (ngoài nhiều bằng danh dự mà ông đạt được sau này). Trên thực tế, cố gắng gọi tên những nhà tiên phong xuất sắc người Anh trong lĩnh vực khoa học máy tính (ngoài Turing) ngay lập tức đưa ra những cái tên như Christopher Strachey, Robin Milner, Peter Landin và Michael Jackson (những người có tầm nhìn xa về kỹ thuật và là bạn học của Hoare tại Oxford), không ai trong số họ, ngoài Hoare, có bằng tiến sĩ. Đó thậm chí không phải là một hiện tượng thuần túy của Anh, vì Bob Floyd, người tiên phong về thuật toán và phương pháp hình thức, cũng nằm trong danh mục này ở Mỹ, cũng như Michel Sintzoff ở Bỉ. Hãy tưởng tượng những nỗ lực của họ trong sự nghiệp học thuật trong hệ thống bị ám ảnh bởi luật lệ ngày nay.

Một thuật toán đẹp và mô tả đẹp của nó

Et pour un cuộc đảo chính d'essai, ce fut un cuộc đảo chính de maître
(“Lần ra mắt của một người mới bắt đầu, đó là một bước đột phá của bậc thầy”, sau Le Cid, Corneille)

Tên tuổi của Hoare bùng nổ trong lĩnh vực khoa học máy tính với việc xuất bản một thuật toán sắp xếp được sử dụng ngày nay trong hàng triệu chương trình, được đặt tên khéo léo là Quicksort [3] [4]. Nhanh chóng vì nó có thể sắp xếp một mảng các phần tử n– nghĩa là sắp xếp lại chúng theo thứ tự giá trị tăng dần – trong hầu hết các trường hợp tỷ lệ thuận với n ghi nhật ký n. Điều đó có nghĩa là thời gian “gần như tuyến tính” (trong đó “tuyến tính” có nghĩa là tỷ lệ thuận với kích thước n) do hàm “log” tăng quá chậm. Để đánh giá cao tầm quan trọng của kết quả này, cần lưu ý rằng nhu cầu sắp xếp danh sách phát sinh trong nhiều, có thể là hầu hết các chương trình, và kích thước n có thể rất lớn. Những ý tưởng đơn giản mà bất kỳ ai cũng có thể nghĩ ra khi phải đối mặt với nhiệm vụ – ví dụ: quét qua mảng, hoán đổi dọc theo bất kỳ phần tử liền kề nào không đúng thứ tự và lặp lại thao tác quét cho đến khi không còn gì để hoán đổi – là “bậc hai”, nghĩa là chúng mất thời gian tỷ lệ với bình phương của n. Sự khác biệt giữa tuyến tính (hoặc “gần như” tuyến tính) và bậc hai là rất lớn đối với n lớn, ngay cả với các máy tính mạnh mẽ; nó có thể tạo ra sự khác biệt giữa một mảng mà chúng ta có thể sắp xếp trong chớp mắt và một mảng mà chúng ta không sắp xếp vào bất kỳ thời điểm hợp lý nào.

Quicksort nổi bật ở sự đơn giản và sang trọng. Nó dựa trên ý tưởng rằng tồn tại một giải pháp thời gian tuyến tính đơn giản cho một dạng vấn đề sắp xếp hạn chế hơn, mà Hoare gọi là “phân vùng” mảng: sắp xếp lại mảng để các giá trị nhỏ hơn xuất hiện trước, theo sau là các giá trị lớn hơn. Nếu chúng tôi có thể làm điều này thì chúng tôi vẫn chưa sắp xếp mảng, nhưng chúng tôi đã thực hiện một bước tiến lớn, vì hai phần của phân vùng, mỗi phần được lấy trên toàn cầu, tại vị trí cuối cùng của chúng trong mảng được sắp xếp trong tương lai. Và chúng đều nhỏ hơn bản gốc! Vì vậy, tất cả những gì chúng ta phải làm là lặp lại quy trình cho đến khi chúng ta nhận được các lát có kích thước 1 (hoặc 0) và mảng sẽ được sắp xếp.

Làm thế nào để chúng ta phân vùng mảng? Đầu tiên, để xác định “nhỏ hơn” và “lớn hơn”, chúng ta chỉ cần chọn một giá trị, được gọi là “trục”. Nhỏ có nghĩa là nhỏ hơn trục, lớn có nghĩa là lớn hơn. Thuật toán phân vùng, chìa khóa của Quicksort, hoạt động như sau: chúng ta bắt đầu từ bên trái của mảng (nơi cuối cùng chúng ta chỉ muốn các phần tử nhỏ) và di chuyển con trỏ sang phải, dừng lại khi tìm thấy phần tử lớn. Một cách đối xứng, chúng ta bắt đầu một con trỏ khác từ bên phải và di chuyển sang trái cho đến khi tìm thấy một phần tử nhỏ. Nếu hai con trỏ giao nhau thì chúng ta đã hoàn tất: mảng đã được phân vùng. Nếu không, chúng tôi hoán đổi hai phần tử không đúng vị trí và tiếp tục quá trình, cả hai con trỏ đều chọn vị trí chúng đã dừng. Thời gian phân vùng rõ ràng là tuyến tính vì chúng tôi kiểm tra từng phần tử chỉ một lần (con trỏ không bao giờ quay lại).

Để chuyển từ thuật toán Phân vùng sang thuật toán sắp xếp, như đã lưu ý, chỉ cần áp dụng lại thuật toán đó cho các lát cắt là đủ. Quicksort ra đời vào thời điểm Algol 60, người có ảnh hưởng nền tảng đối với Tony Hoare cũng như đối với nhiều người vào thời điểm đó, đã tạo ra đệ quy và một công cụ mới thú vị. Quicksort cung cấp cách sử dụng đệ quy tự nhiên: bạn có thể triển khai quy trình Quicksort bằng cách gọi Phân vùng trên mảng hai dấu chỉ mục a và b (ban đầu là 1 và n), từ đó tạo ra dòng phân vùng i, sau đó gọi lại Quicksort trên mỗi lát trong số hai lát. Trong nhiều thập kỷ, các khóa học về khoa học máy tính đã sử dụng các mô tả về Quicksort không chỉ như một thuật toán mà còn như một ví dụ về lý do tại sao đệ quy lại hữu ích. (Leslie Lamport gần đây đã chỉ ra rằng đệ quy là một tính năng ngẫu nhiên chứ không phải là tính năng thiết yếu của Quicksort [5].) Mô tả thuật toán đầy đủ trong [2] là:

nếu M < N sau đó bắt đầu phân vùng (A, M, N, I, J); sắp xếp nhanh (A, M, J); sắp xếp nhanh (A, I, N) kết thúc

(trong đó A là mảng và M, N là giới hạn tổng thể của nó).

Ngoài sự khéo léo và thiết thực của giải pháp, sự tinh tế trong mô tả ban đầu [3] đã thu hút sự chú ý của mọi người. Mặc dù nó không chứa bằng chứng về tính đúng đắn nhưng nó được cấu trúc theo cách mà các báo cáo xác minh của những người khác sẽ sớm tuân theo.

Quicksort cũng đánh dấu sự chuyển đổi từ nền tảng nhân văn sang toán học và khoa học. Hoare đã học tiếng Nga và, vào thời kỳ đỉnh điểm của Chiến tranh Lạnh, đã dành một năm ở Moscow (không ai khác ngoài Andrey Kolmogorov) để thực hiện một nhiệm vụ chính thức, tôi tin rằng một phần tập trung vào những nỗ lực ban đầu về dịch máy. Mặc dù rõ ràng là anh ấy không giải quyết được vấn đề đó, nhưng anh ấy đã nghĩ ra Quicksort để có thể xử lý danh sách các từ tiếng Nga trong bộ nhớ (chứ không phải trên băng). Theo Hoare (như đã nói với Cliff Jones), anh ấy không thể biết cách diễn đạt thuật toán cho đến khi tham gia khóa học Algol 60 và mọi thứ đã ổn thỏa.

Ngữ nghĩa tiên đề

Quicksort, dù xuất sắc và hữu ích đến đâu, cũng chỉ là một thuật toán. Đóng góp lớn tiếp theo của Hoare là mang tính nền tảng; nó bắt đầu một lĩnh vực phát triển hoàn toàn mới

Ngay từ khi bắt đầu có máy tính, nhiều người đã thấy rõ rằng tác động của các chương trình có thể được mô tả bằng toán học; Chính Turing đã viết một ghi chú thuyết phục về chủ đề này, giới thiệu thuật ngữ “khẳng định” [6] [7]. Công việc đáng kể được tiến hành vào những năm 1960 về lập trình toán học; không quá nhiều về cú pháp (một vấn đề phần lớn được đề cập trong công trình của Chomsky, ban đầu dành cho ngôn ngữ học của con người) mà là ngữ nghĩa, được phản ánh cụ thể trong một hội nghị năm 1964 ở Vienna (cuốn sách xuất hiện năm 1966 [8]), nhưng việc sử dụng các hình thức này vẫn không thực tế. Một bước tiến lớn đã xảy ra với bài báo năm 1967 của Floyd liên kết các khẳng định, theo nghĩa của Turing, với các vị trí trong chương trình [9]. Trong một trong những bài viết nổi tiếng nhất của mình [10], Hoare đã biến ý tưởng của Floyd thành một lý thuyết tiên đề chính thức, khai sinh ra "ngữ nghĩa tiên đề", ngày nay còn được gọi là "logic Hoare" [11] [12].

Ý tưởng, dựa trên các nguyên tắc logic toán học, thật tuyệt vời: định nghĩa ngôn ngữ lập trình là một lý thuyết toán học – dọc theo dòng hệ thống tiên đề được giới thiệu bởi những người như Russell, Zermelo, Fraenkel, Von Neumann và Bernays vào đầu thế kỷ 20^th thế kỷ – để cho phép chứng minh các thuộc tính chứng minh của bất kỳ chương trình nào bằng ngôn ngữ, chẳng hạn

{n > 5} if m < -3 thì n := n + m else n := n – 2 end {n > 1

Công thức này (tùy thuộc vào bằng chứng hoặc bác bỏ về mặt lý thuyết) được gọi là “Bộ ba Hoare”, {P} A {Q}, biểu thị rằng việc thực thi A bắt đầu ở trạng thái thỏa mãn P sẽ mang lại trạng thái thỏa mãn Q. Ở đây, nếu chúng ta bắt đầu với n lớn hơn 5 thì chúng ta sẽ kết thúc với n lớn hơn 4. (Và không, không có lỗi đánh máy trong ví dụ này. Bộ ba không phải là bộ ba mạnh nhất mà chúng ta có thể rút ra nhưng nó đúng.) Cách thức hoạt động của lý thuyết này là bao gồm một tiên đề hoặc quy tắc suy luận cho mọi cấu trúc của ngôn ngữ; ví dụ tiên đề cho phép gán (“:=”) là {P [E / n]} n := E {P}, tính ngược, trong đó P [E / n} biểu thị khẳng định P trong đó mọi lần xuất hiện của n đã được thay thế bằng biểu thức E, về mặt văn bản (một khái niệm xuất phát từ phép tính lambda, do Church và Curry thiết kế vào những năm 1930, và hoạt động cho dù E có bao gồm các lần xuất hiện của n hay không, như trong ví dụ n := n + m ở trên).

Cái hay của phương pháp này là các quy tắc được xác định theo cách hoàn toàn hình thức, nghĩa là chúng hoạt động một cách máy móc trên văn bản chương trình. Bạn có thể áp dụng chúng một cách mù quáng mà không cần trực giác (“chương trình thực hiện điều này hoặc điều kia”) và bạn có thể yêu cầu một chương trình máy tính – người xác minh chương trình – áp dụng chúng cho bạn. Trong 50 năm tiếp theo, cho đến nay, các hệ thống chứng minh chương trình đã được xây dựng theo cách tiếp cận được giới thiệu trong bài báo này và những cải tiến về mặt lý thuyết sau này của chính Hoare, Dijkstra và những người khác.

Bài viết gốc bao gồm các quy tắc cho các cấu trúc lập trình đơn giản. Trong những năm tiếp theo, Hoare đã mở rộng lý thuyết sang các cơ chế thách thức hơn: quy trình và đệ quy [2] (từ đó có đoạn trích ở đầu bài viết này), cấu trúc dữ liệu [13]. Bài viết thứ hai rất đáng chú ý vì nó chứa đựng sự xuất hiện đầu tiên – một bài duy nhất, không có nhiều bình luận – về khái niệm cơ bản về bất biến lớp.

Ứng dụng trong thiết kế ngôn ngữ

Mặc dù phần lớn là một nhà lý thuyết sau khi bắt đầu sự nghiệp học thuật với các giảng viên ở Belfast rồi Oxford, Hoare luôn sẵn sàng áp dụng các ý tưởng của mình, có lẽ một phần vì kiến thức nền tảng về ngành của anh ấy. Anh tham gia vào lĩnh vực thiết kế ngôn ngữ, giúp Niklaus Wirth [14] thiết kế Algol W [15] bằng cách đưa ra khái niệm về bản ghi (“cấu trúc” trong C), một phát minh ngôn ngữ lập trình mà ông tự hào vì nó mang đến cho phía dữ liệu cùng một loại cơ chế cấu trúc đã rất thành công ở phía điều khiển, với các cấu trúc điều khiển của “lập trình có cấu trúc”. Algol W là sự tiếp nối và đơn giản hóa (quan trọng nhất) của Algol 60. Nó đã được sử dụng một thời gian làm ngôn ngữ lập trình giảng dạy tại Stanford và đó là ngôn ngữ lập trình thực sự đầu tiên của tôi yêu thích, từ đó tôi đã học được rất nhiều điều (và khiến tôi không thể chuyển sang ngôn ngữ kế nhiệm của chính nó, Pascal của Wirth). Hoare muốn chỉ ra rằng anh ấy đã thiết kế các cấu trúc ngôn ngữ lập trình nhưng chưa bao giờ là một ngôn ngữ lập trình chính thức, vì anh ấy (theo quan điểm riêng của mình) không giỏi hoàn thiện các chi tiết. Ví dụ: khi anh ấy nghĩ ra các cơ chế đồng thời mạnh mẽ (với CSP, được thảo luận bên dưới), những người khác đã biến ý tưởng thành cấu trúc ngôn ngữ lập trình thực tế cho các ngôn ngữ Occam và Ada.

Bao gồm Algol W, cùng với các bản ghi, tham chiếu (con trỏ), bao gồm cả khả năng có con trỏ rỗng. Nhiều năm sau, Hoare tuyên bố rằng đó là “sai lầm tỷ đô” của mình [16]. Để tiếp tục trích dẫn các nhà viết kịch Pháp (đối thủ) của thế kỷ 17^th, theo ý kiến ​​​​của tôi, Hoare xứng đáng, đối với thiết kế đặc biệt này, Ni cet excès d'honneur, ni cette indignité (Racine, Britannicus): không quá danh dự cũng không phải sự sỉ nhục như vậy. Đầu tiên, con trỏ null về cơ bản là không thể tránh khỏi nếu bạn muốn mô hình hóa thế giới có tham chiếu (những thứ chứa ký hiệu của những thứ khác). Thứ hai, con trỏ null ít nhất cũng lùi về phía NIL trong McCarthy's Lisp (1959) nên lỗi, nếu có, sẽ được chia sẻ.

Một cách khác mà Hoare xắn tay áo lý thuyết của mình để giải quyết vấn đề thực tế là hợp tác với Niklaus Wirth để cung cấp một định nghĩa ngữ nghĩa tiên đề (dĩ nhiên là dựa trên công trình được đề cập ở trên) cho một phần của ngôn ngữ Pascal [17].

Một trường hợp công việc thực tế khác là việc anh tham gia vào lĩnh vực mà sau này trở thành ngôn ngữ lập trình Ada. Vào giữa những năm 1970, Bộ Quốc phòng Hoa Kỳ đã tổ chức đấu thầu thiết kế một ngôn ngữ lập trình tiêu chuẩn. Bốn đội, được mã hóa bằng màu sắc nhằm tạo ra một sân chơi bình đẳng, đã lọt vào vòng hai. Hoare và Wirth đã tham khảo ý kiến ​​cho đề xuất “Vàng”, nhưng đề xuất này đã thua thiết kế “Xanh” của Jean Ichbiah. Vẫn còn một vòng nữa, liên quan đến thiết kế Xanh cũng như Đỏ. Vào thời điểm đó, tôi đã có một chút thay đổi trong câu chuyện. Tôi đã tổ chức một khóa học hè về lập trình – hóa ra đó lại là một sự kiện đáng nhớ, diễn ra vào tháng 7 năm 1978, với ba giảng viên: Hoare, Barry Boehm (gia đình họ trở nên rất thân thiết vào dịp đó trong nhiều năm sau đó) và Jean-Raymond Abrial. Tôi nghĩ chúng tôi đã tổ chức một cuộc họp chuẩn bị vào mùa xuân năm trước, vào tháng 3, với bữa tối tại một nhà hàng tuyệt vời ở Paris. Ichbiah rất muốn tranh thủ sự giúp đỡ của Hoare trong vòng chung kết, đã cố gắng mời mình đi ăn tối, chiếm chỗ ngồi cạnh Hoare và suốt buổi tối tán tỉnh anh ta với cường độ không còn chỗ cho những vị khách khác nói gì. Hộp thoại chủ yếu là “Tôi đã thua một lần, tôi không muốn liên quan đến trận thua thứ hai!” so với “đây là cơ hội để bạn xóa tình tiết đó và ra đi thành công!”. Tôi nghĩ điều Ichbiah mong muốn nhất từ ​​Hoare là sự giúp đỡ trong việc thiết kế cơ chế tương tranh. Thật vậy, cơ chế đồng thời “điểm hẹn” cuối cùng của Ada phần lớn bắt nguồn từ CSP của Hoare (được thảo luận bên dưới), vừa xuất hiện vào thời điểm đó.

Cuối cùng Hoare không trực tiếp tham gia thiết kế mà được đưa vào danh sách thành viên ủy ban cố vấn cho việc thiết kế đó. Vai trò đó và việc sử dụng các ý tưởng CSP của ông đã không ngăn cản ông chỉ trích thiết kế của Ada một cách khá gay gắt trong bài giảng Giải thưởng Turing [1].

Phương pháp lập trình

Trong những năm trước đó – đặc biệt là những năm 1970 – giới chuyên môn coi Hoare là người đề xướng phương pháp lập trình có kỷ luật. Mọi người đã nhận ra rằng phát triển phần mềm cần có các nguyên tắc kỹ thuật. Người đề xuất chính của trường phái đó là Edsger Dijkstra, được Hoare và Wirth đồng hành trong tâm trí công chúng, cũng như những nhân vật quan trọng như David Gries, David Parnas và Harlan Mills. Động lực đến từ việc xuất bản cuốn sách Lập trình có cấu trúc [18], bao gồm ba chuyên khảo; phần đầu tiên về lập trình có cấu trúc của Dijkstra, mở rộng dựa trên một số đóng góp trước đây của ông và các cấu trúc điều khiển được đề cập; bài thứ hai là của Hoare về cấu trúc dữ liệu. Cuốn thứ ba, của Hoare và nhà khoa học máy tính người Na Uy Ole-Johan Dahl, người đồng sáng tạo ra Simula 67, có tựa đề lạ lùng nhưng thực sự là phần giới thiệu, lần đầu tiên, về các ý tưởng của lập trình hướng đối tượng. Hoare là người có công trong việc viết lại văn xuôi của Dahl sang tiếng Anh chuẩn hơn.

Mọi người trong nghề đều đọc cuốn sách vào thời điểm nó được xuất bản. Hầu hết mọi người dừng lại ở chương đầu tiên hoặc chương thứ hai và thấy chương thứ ba hơi khó hiểu. Khi còn là sinh viên, tôi được khuyên nên đọc cuốn sách và yêu thích chương thứ ba, điều này cho tôi cơ hội tuyệt vời để khám phá OOP trước khi hầu hết mọi người chú ý đến nó. Một trong nhiều cách mà tôi mang ơn Tony.

Đồng thời

Một số vấn đề khó nhất trong lập trình phát sinh khi chúng ta xử lý một số tính toán xảy ra song song, gây ra các vấn đề về đồng bộ hóa và giao tiếp. Vào những năm 70, các vấn đề này đã thu hút một số bộ óc giỏi nhất trong lĩnh vực này, bao gồm Dijkstra và Lamport. Thách thức là tìm ra, đối với lập trình đồng thời, các cơ chế có cùng mức độ rõ ràng, trừu tượng, dễ hiểu và có thể chứng minh được như lập trình tuần tự. (Ví dụ, Dijkstra không thích chút nào khi mọi người nhận xét đùa rằng semaphores, phát minh của ông về lập trình đồng thời, có cùng mức độ trừu tượng thấp như đối tượng mà ông coi thường trong lập trình tuần tự, các hướng dẫn goto.)

Một cải tiến đáng kể là sự ra đời của cấu trúc ngôn ngữ lập trình, màn hình [19]. (Per Brinch Hansen đã xuất bản một bài báo về màn hình cùng lúc; tôi không biết liệu vấn đề về quyền ưu tiên đã được giải quyết chưa.) Màn hình là một mô-đun tập hợp một tập hợp các hoạt động có thể xảy ra đồng thời trên một tài nguyên. Tuy nhiên, màn hình chỉ là một cấu trúc ngôn ngữ và thiếu thông số kỹ thuật chính thức mà người ta cần phải suy luận một cách chặt chẽ về các chương trình đồng thời.

Hoare cảm thấy cần có sự trừu tượng hơn, tránh xa cấu trúc của ngôn ngữ lập trình. Do đó, phiên bản đầu tiên của Quy trình giao tiếp tuần tự (CSP), được xuất bản năm 1978 [20]. Một cái nhìn sâu sắc quan trọng vào thời điểm đó là xem xét hai thách thức cốt lõi của tính đồng thời, đồng bộ hóa và giao tiếp và quyết định xem điều gì là quan trọng nhất. Nếu bạn có các hoạt động khác nhau (như tiến trình hoặc luồng) diễn ra song song, đôi khi chúng phải đồng bộ hóa với nhau, chẳng hạn như khi chúng cần quyền truy cập vào tài nguyên chia sẻ có giới hạn như máy in hoặc đường dây liên lạc; và đôi khi chúng phải truyền đạt dữ liệu với nhau. Quyết định trong CSP ban đầu là coi giao tiếp là hoạt động nguyên thủy, dựa trên quan sát rằng để P gửi một số dữ liệu và Q nhận nó thì cả hai đều phải sẵn sàng cho việc đó; nói cách khác, họ phải đồng bộ hóa. Khi đó, giao tiếp hàm ý sự đồng bộ hóa (nhưng không phải ngược lại). Do đó có chữ “C” để giao tiếp trong CSP. Các quy trình (“P”) có thể sử dụng kênh để liên lạc. Hai thao tác cơ bản mà một quy trình có thể tham gia là đầu ra và đầu vào, được viết (đối với kênh c):

c!x — Đầu ra x trên kênh c

c?x — Đợi đầu vào x đi qua kênh c

Thành phần CSP quan trọng trong việc sử dụng các cơ chế này là tính không xác định, một phần là kết quả từ công trình “Kỷ luật lập trình” của Dijkstra [21]. (Chắc chắn các nhà sử học khoa học sẽ nghiên cứu những ảnh hưởng qua lại giữa Hoare và Dijkstra trong những năm đó, bao gồm cả việc Dijkstra mở rộng logic Hoare thành “phép tính các điều kiện tiên quyết yếu nhất” trong cùng một tác phẩm [21] .) Tính không xác định, sử dụng ký hiệu Dijktra P [] Q (thực hiện P hoặc Q) áp dụng cụ thể cho đầu vào: bạn có thể viết một cái gì đó như

c1?x 🡪 op1 (x) []

c2?x 🡪 op2 (x)

nghĩa là: nhận giá trị từ kênh c1 hoặc kênh c2, tùy theo điều kiện nào đến trước và thực hiện điều gì đó (khác) với nó. Cơ chế Rendezvous của Ada triển khai ý tưởng này dưới dạng cấu trúc lập trình.

Chúng tôi có vinh dự được nghe một trong những bài thuyết trình đầu tiên về CSP tại trường hè năm 1978; Lúc đó Hoare mới thiết kế nó và dành toàn bộ bài giảng của mình cho nó.

Tôi đã đề cập đến phong cách không thể bắt chước của Hoare và đây là một ví dụ từ những bài giảng đó. Lời giải thích của ông về cấu trúc không xác định ở trên diễn ra như thế này. Khi bạn đang đợi xe buýt, anh ấy hỏi. làm sao bạn có thể chờ nhanh hơn? Khán giả có thể hiểu được sự ngạc nhiên và không nói gì. Anh ấy tiếp tục, câu trả lời là đợi nhiều hơn một xe buýt cùng một lúc. Ví dụ: bạn đang ở Peartree ở Oxford và muốn đến ga chính, bạn có thể sử dụng tuyến 300 (Park & ​​Ride) hoặc S2 (Stagecoach). Bạn có thể chọn một trong số chúng và đợi xe buýt của nó hoặc bạn có thể “đợi nhanh hơn” bằng cách đợi cho đến khi chiếc xe buýt đầu tiên xuất hiện, từ một trong hai tuyến xe buýt này. Đó là bản chất của cấu trúc đầu vào không xác định CSP.

Tony Hoare, trường hè Marktoberdorff, tháng 8 năm 2004

Trong công việc CSP tiếp theo của mình vào những năm 1980, Hoare tiếp tục rời xa các ngôn ngữ lập trình và tạo ra CSP tổng quát hơn (giữ từ viết tắt nhưng ngừng mở rộng nó vì nó dần trở nên không chỉ là các quy trình tuần tự và giao tiếp của chúng). CSP đã trở thành một trong số “các phép tính” - một phép tính nổi tiếng khác là CCS của Milner, Phép tính các hệ thống giao tiếp - cung cấp các khuôn khổ đại số để mô tả các phép tính tổng quát. CSP mới đã được Hoare [22] mô tả trong một cuốn sách mặc dù bạn có thể tìm thấy mô tả sâu rộng và cập nhật hơn trong cuốn sách của chính Bill Roscoe [23].

Để mô tả các tính toán, CSP mới sử dụng một tập hợp nhỏ các toán tử nguyên thủy dùng để kết hợp các quy trình. Trong số các toán tử quan trọng nhất là lựa chọn bên ngoài P 🞏 Q (môi trường quyết định đưa ra cho bạn P hoặc Q và bạn phải đối phó với bất cứ điều gì xảy ra, gần như theo truyền thống về tính không tất định của CSP ban đầu), lựa chọn bên trong P Π Q (bạn có thể quyết định thực hiện P hoặc Q), thao tác song song P ||_E Q (thực hiện song song P và Q, đồng bộ hóa trên một số sự kiện đã thỏa thuận, các thành viên của E), ẩn (cho phép bạn chọn mức độ trừu tượng của mình bằng cách bỏ qua một số sự kiện) và đệ quy. Sau đó, theo truyền thống của công trình Ngữ nghĩa tiên đề năm 1969 của Hoare, lý thuyết này khẳng định một số tiên đề mô tả các thuộc tính hình thức của các toán tử này, chẳng hạn như tính giao hoán và tính kết hợp. Trong suốt tác phẩm của mình, Hoare là người ủng hộ phương pháp tiên đề do Russell tiên phong, người đã mô tả nó là “tất cả những lợi thế của hành vi trộm cắp so với công việc lương thiện” – một trong những điểm mà nhà bình luận sinh ra ở nước ngoài phải thừa nhận rằng một số tính hài hước cực đoan hơn của người Anh sẽ mãi mãi không thể xuyên thủng đối với phần còn lại của nhân loại.

Người dẫn đầu và người xúc tác

Các nhà toán học cũng giống như người Pháp: bạn cho họ thứ gì đó
họ dịch nó sang ngôn ngữ của họ và nó trở thành một thứ hoàn toàn khác.
Goethe

CSP đã khơi dậy sự quan tâm thực sự đến các phương pháp hình thức và tính đồng thời, đặc biệt là trong số các nhà nghiên cứu đã từng làm việc tại Nhóm Nghiên cứu Lập trình Oxford huyền thoại của Hoare. Hoare, được đào tạo tại Merton College ở Oxford, trở lại làm giáo sư vào năm 1977, tiếp quản nhà tiên phong về khoa học máy tính Christopher Strachey (một nhân vật hấp dẫn khác, mang đậm chất Anh). Hoare có tài năng phi thường trong việc thu hút những người xuất sắc và giúp họ phát huy thế mạnh của mình. Ví dụ, vào đầu những năm tám mươi, ông đã đưa đến Oxford những người sáng tạo ra hai ngôn ngữ đặc tả hình thức chính: Cliff Jones với VDM [24], Jean-Raymond Abrial với Z [25]. Tại Oxford, Z thực sự đã trải qua một quá trình làm lại có hệ thống, gợi nhớ đến câu châm ngôn của Goethe [26] được sao chép ở trên, trong đó người Pháp và các nhà toán học được thay thế bằng các nhà toán học (hoặc nhà khoa học máy tính) người Anh. Phiên bản mới đã đạt được thành công to lớn ở Anh, giành được Giải thưởng Nữ hoàng và không chỉ được sử dụng trong học thuật mà còn trong nhiều ứng dụng quan trọng trong công nghiệp, dẫn đến một số công ty khởi nghiệp và công việc của các nhà nghiên cứu như vậy (tất cả đều đã từng học qua Oxford) như Jim Woodcock, Carroll Morgan, Jim Davies, J. Michael Spivey, Ian Hayes và Ib Holm Sørensen [27].

Một ví dụ khác về hậu quả của môi trường trí tuệ đặc biệt tại Oxford vào thời điểm đó là công trình của Cliff Jones về bảo đảm độ tin cậy, một phần mở rộng của logic Hoare cho sự tương tranh [28].

Một số nhà khoa học đã vĩ đại theo cách riêng của họ; một số còn là những nhà quản lý giỏi, lãnh đạo các trường khoa học và để lại ảnh hưởng sâu sắc đến sự nghiệp của nhiều người. Ví dụ về việc ai đó để lại cả hai loại di sản vẫn tồn tại (như David Hilbert) nhưng không thường xuyên. Hoare là một trong số họ. Một dấu hiệu cho thấy vai trò lãnh đạo của ông là vai trò biên tập của ông trong “Loạt bài Khoa học Máy tính” của Prentice Hall, tạp chí đã xuất bản hàng chục đầu sách có ảnh hưởng về lý thuyết, ngôn ngữ lập trình, ngữ nghĩa và phương pháp lập trình trong những năm 1980 và 1990, với sự hỗ trợ của một biên tập viên vĩ đại, Helen Martin, người mới chỉ 20 tuổi khi bắt đầu. (Nhiều cuốn sách của Prentice Hall được trích dẫn trong thư mục là từ bộ sách đó.) Nói chung, ông đã trao đổi thư từ với nhiều người, đặc biệt là các nhà khoa học trẻ, và hướng dẫn họ trong sự nghiệp. Một trong những trải nghiệm thú vị và mang tính giáo dục tại nhiều hội thảo khác nhau được tổ chức để vinh danh ông, đặc biệt nhân dịp ông được cho là “nghỉ hưu” liên tiếp [29] [30] , là để ai đó giải thích trong cuộc trò chuyện nào đó rằng anh ta có mối quan hệ đặc biệt với Tony, và phát hiện ra rằng mọi người khác trong nhóm cũng nghĩ giống hệt như vậy. Ông thực sự quan tâm và theo đuổi trong nhiều năm sự phát triển trí tuệ của người khác. Hãy để tôi trích dẫn một ví dụ cá nhân. Sau khi tôi đăng một số nhận xét phê bình về các ngôn ngữ được cho là hướng đối tượng, anh ấy đã viết thư để khiển trách tôi (29 tháng 8 năm 2002):

Tôi đã chịu ảnh hưởng nhiều từ Peter Medawar và Richard Doll trong việc tìm ra thái độ cảm xúc của riêng mình đối với các vấn đề mà bạn thảo luận. Medawar nói rằng nhà khoa học chân chính luôn ca ngợi công trình của những người đi trước và chỉ ra mọi khuyết điểm của chính mình. Tôi biện minh cho điều này bằng cách so sánh với thế giới điện ảnh: trên phim trường, mức độ căng thẳng lớn đến mức mọi người đều rất thân thiện với nhau, ngay từ cái tên đầu tiên, ‘em yêu..’, ‘điều đó thật tuyệt vời nhưng..’. Đó là cách duy nhất để vượt qua căng thẳng và xây dựng sự tự tin cho mọi người. Nghiên cứu là một công việc làm mất tinh thần không kém và cần có những quy ước tương tự.

Mặc dù (như tôi đã chỉ ra cho anh ấy) rằng lời khuyên đó không hoàn toàn phù hợp với lời chỉ trích của anh ấy đối với Ada trong bài giảng Giải thưởng Turing, nhưng tôi đã ghi nhớ bài học này, bao gồm cả khuyến nghị của chính anh ấy trong cùng một thông điệp về việc đánh giá thấp đóng góp của chính mình và ghi nhận quá mức những đóng góp của người khác, điều mà tôi thường nhắc lại với các sinh viên (như xu hướng tự nhiên trong một bài báo trình bày tác phẩm mới nhất và vĩ đại nhất của bạn là làm điều ngược lại).

Một ví dụ khác về vai trò là chất xúc tác của anh ấy, tôi nhớ rất rõ khi đến thăm anh ấy ở Oxford vào khoảng năm 1984, và có một bài nói chuyện trong đó về cơ bản anh ấy chỉ là khán giả, cùng với tối đa hai hoặc ba người khác (một dấu hiệu khác cho thấy anh ấy sẵn sàng và sẵn sàng lắng nghe ý kiến của người khác, cho dù anh ấy có thể bận rộn với cả nghiên cứu và hoạt động quản lý). Bối cảnh là tôi đã xuất bản một chuyên luận về lập trình và sách giáo khoa bằng tiếng Pháp vào năm 1978, mà tôi đã cho anh ấy xem nhân dịp học hè, sau đó anh ấy ngay lập tức nói rằng tôi nên xuất bản bản dịch trong bộ truyện Prentice Hall của anh ấy. Khi tôi hỏi liệu anh ấy có biết người dịch nào không, anh ấy trả lời rằng tôi nên tự dịch, điều mà tôi chấp nhận một cách ngu ngốc vì điều hiển nhiên đã xảy ra: thay vì dịch, tôi bắt đầu tạo ra một thứ hoàn toàn mới, một phần trong số đó tôi sẽ trình bày vào ngày hôm đó ở Oxford. Để giải thích những gì tôi đang làm trong kiến ​​trúc phần mềm dựa trên logic, tôi đã tìm kiếm một phép ẩn dụ hay và ngay lập tức đề xuất rằng có một loại “hợp đồng” giữa người gọi và người được gọi. Anh ấy không nói gì, nhưng sự hiện diện đơn thuần của anh ấy đã giúp tôi làm cho những ý tưởng mới chớm nở của mình trở nên sôi nổi. Nhiều người có thể kể lại những trải nghiệm tương tự.

Là một trường hợp khác cho thấy Hoare đã vươn xa hơn những đóng góp của chính mình, anh ấy là nhân vật chủ chốt trong IFIP (Liên đoàn xử lý thông tin quốc tế) Nhóm làm việc 2.3 về phương pháp lập trình. IFIP WG là một loại câu lạc bộ thảo luận khoa học có sự đồng tham gia. Một trong những WG ban đầu là 2.1, chịu trách nhiệm phát triển phiên bản kế thừa cho các ngôn ngữ lập trình Algol 58 và Algol 1960 có nguồn gốc IFIP và có ảnh hưởng to lớn. WG 2.1 chuyển sang sản xuất một ngôn ngữ cực kỳ mạnh mẽ, trở thành Algol 68. Wirth, được Hoare hỗ trợ, đã đề xuất một thiết kế mới đơn giản hơn nhiều, Algol W (mà tôi đã thảo luận ở trên). Sau khi bị nhóm này từ chối, một số người bất đồng chính kiến ​​bao gồm Wirth, Dijkstra và Hoare đã thành lập một nhóm nhỏ, 2.3, chuyên về phương pháp lập trình, hiện đã tổ chức 71 cuộc họp kể từ cuộc họp đầu tiên ở Oslo năm 1969!. Hoare là thành viên tích cực của WG 2.3 kể từ khi thành lập, tham dự các cuộc họp của nhóm cho đến gần đây, tức là trong hơn nửa thế kỷ; WG2.3 là một địa điểm khác mà ông đã gây ảnh hưởng và đưa ra lời khuyên cho nhiều thế hệ nhà nghiên cứu.

Quay lại học

J'ai plus de quà lưu niệm que si j'avais mille ans
Baudelaire, Les Fleurs du Mal
(“Tôi có nhiều kỷ niệm hơn cả khi tôi ngàn tuổi”)

Sau khi nghỉ hưu tại Đại học Oxford vào năm 1999, Hoare chuyển ngay sang Microsoft Research với tư cách là Nhà nghiên cứu chính tại phòng thí nghiệm mới thành lập ở Anh do Roger Needham chỉ đạo. Làm nhiều người ngạc nhiên (vì anh ấy luôn nổi tiếng là một người đàn ông Oxford), việc chuyển đến cũng là đến Cambridge, nơi đặt trụ sở của liên doanh mới. Cambridge MSR nhanh chóng trở thành một trong những phòng thí nghiệm khoa học máy tính uy tín nhất thế giới.

Động thái đó cũng trùng hợp với điều mà một số người coi là sự thay đổi thái độ. Hoare, cùng với Dijkstra, Wirth và những người khác, đã gắn liền với phong trào phương pháp lập trình của những năm 1970, hàm ý đúng hay sai đối với nhiều người về ý tưởng về thái độ kỷ luật đối với lập trình. Vào thời điểm chuyển sang Microsoft, anh ấy đã trở nên hòa hợp hơn với những hạn chế của ngành và nhu cầu xử lý các chương trình như hiện tại, chứ không chỉ với các chương trình như chúng phải vậy. Tôi nhớ đã nghe anh ấy nói đùa – trong một cuộc thảo luận thân mật trong giờ giải lao – rằng “Java nên được coi là một trong những quy luật tự nhiên” (không phải điều gì đó mà tôi sẽ không bao giờ đồng ý). Ông đặc biệt quan tâm đến sức nặng của mã kế thừa, tất cả hành trang đó được tích lũy qua nhiều thập kỷ lập trình ít nhiều cẩn thận (đối với tôi, tôi nhớ lại câu thơ của Baudelaire). Trong email gửi cho tôi được trích dẫn trước đó, anh ấy viết:

Tôi cũng nên khen ngợi cách tiếp cận khác là thiết kế thư viện tốt hơn và ngôn ngữ tốt hơn. Cả bạn và Niklaus [Wirth] đều có cùng quan điểm. Đó phải là con đường đúng đắn về lâu dài. Nhưng trước khi điều này có hiệu lực, bạn sẽ cần phải viết lại rất nhiều chức năng của mã kế thừa. Vì vậy, bạn sẽ cần phải tìm hiểu xem mã kế thừa thực sự làm gì. Dự án của tôi có thể giúp thực hiện điều này.

và kết luận bằng một công thức khiến tôi ấn tượng: “Đó là lý do tại sao tôi có quan điểm hơi trung gian – bạn có thể nói là 'ăn tối với ma quỷ'. Chà, có lẽ ai đó cũng phải làm điều đó”. Anh ấy đã chọn chủ nghĩa thực dụng.

Điều khiến tôi ấn tượng nhất trong những năm đó (đầu những năm 2000, khi ông đã bước vào tuổi bảy mươi) là lòng ham học hỏi không ngừng nghỉ của ông. Đó không phải là điều gì mới mẻ: năm này qua năm khác, hết hội nghị này đến hội nghị khác, ông luôn ngồi ở hàng ghế đầu tiên, với cuốn sổ lớn màu đen, cẩn thận ghi lại những gì diễn giả đang nói. Điều đáng chú ý hơn là rất nhiều người khác, rõ ràng là đang bận tâm đến những công việc cực kỳ quan trọng, lại tiếp tục hack máy tính xách tay của họ (sau này là điện thoại). Ông có nhiều trách nhiệm như bất kỳ ai khác, chưa kể đến Giải thưởng Turing, giải thưởng Kyoto và khoảng 15 bằng tiến sĩ danh dự, nhưng khi có cơ hội học hỏi từ những người khác, ông đã sử dụng nó mà không thỏa hiệp hay phân tâm.

Tôi gặp anh ấy tại Microsoft Research ở Redmond trong một phòng họp nhỏ, lắng nghe một kỹ sư trẻ đang trình bày một số vấn đề phức tạp của các công cụ .NET. Tony đang hỏi những câu hỏi đầy kiên nhẫn để đảm bảo rằng anh ấy hiểu được chi tiết. Tôi tin rằng sự kết hợp đặc biệt này, điều mà tôi thấy ở rất ít người, là một trong những dấu hiệu của một nhà khoa học vĩ đại: sự kết hợp đặc biệt giữa lòng kiêu hãnh và sự khiêm tốn. Khiêm tốn không có nghĩa là khiêm tốn: Hoare ý thức được thành tích và uy tín của mình; nhưng anh ấy khiêm tốn theo nghĩa luôn sẵn sàng quay trở lại ghế trường và bắt đầu học một chủ đề mới.

Thử thách lớn và các lý thuyết thống nhất

Giống như nhiều nhà khoa học có ảnh hưởng, Hoare trở nên bận tâm trong giai đoạn sau của sự nghiệp với các vấn đề có phạm vi chung.

Về mặt lý thuyết, ông lo ngại về sự phong phú của các cách tiếp cận khác nhau để mô tả ngôn ngữ lập trình, bao gồm hai đóng góp quan trọng: của riêng ông, với ngữ nghĩa tiên đề (“Hoare Logic”); và tác phẩm bắt nguồn từ Dana Scott và Christopher Strachey về ngữ nghĩa biểu thị mà ông rất tôn trọng. Các chương trình “nói về” đầu tiên, thể hiện tính chất của chúng; cái thứ hai “định nghĩa” các chương trình như các điểm cố định của các hàm trên các không gian cụ thể. Bất kỳ ai đã xem xét cả hai (hoặc sự kết hợp của chúng theo các cách tiếp cận như cách giải thích trừu tượng của Cousots [31]) đều có trực giác rằng phải có cách nào đó để tích hợp chúng. Đó là mục tiêu trong công việc của Hoare, cùng với He Jifeng, về “Các lý thuyết thống nhất về lập trình” [32]. Mặc dù nó có ảnh hưởng lớn nhưng công việc này, tôi nghĩ (theo tinh thần của ghi chú này là đáng ngưỡng mộ nhưng không phải là thánh tích) rằng nó đã không thực sự thành công trong mục tiêu thống nhất của mình; vẫn cần một cái gì đó cơ bản hơn để giải thích về lập trình.

Một công việc quan trọng khác, trong vai trò không mệt mỏi của Hoare là người tổ chức và xúc tác, là sáng kiến “thử thách lớn đối với trình biên dịch xác minh” của ông. Để phù hợp với công việc nền tảng của mình về tính chính xác của phần mềm, ông đã đề xuất ý tưởng về một dự án lớn dành cho việc sản xuất một công cụ có thể tạo ra các chương trình được đảm bảo chính xác, không chỉ về mặt kiểu chữ, như với trình biên dịch cho bất kỳ ngôn ngữ gõ tĩnh nào, mà còn về mặt ngữ nghĩa của chúng: tính chính xác của kết quả. Sau một thời gian, anh ấy đã loại bỏ thuật ngữ “trình biên dịch” khỏi tên, được coi là quá kỹ thuật đối với nhiều đối tượng (bao gồm cả những người có thể cấp tài trợ), chỉ để lại “Thử thách lớn đối với phần mềm đã được xác minh”. Hội nghị đầu tiên về chủ đề này được tổ chức tại ETH Zurich vào năm 2005, dưới tên VSTTE: “Phần mềm đã được xác minh: Công cụ, Lý thuyết, Thử nghiệm”, với các kỷ yếu được lưu hành rộng rãi [33]. Kể từ đó, hội nghị đã có thêm nhiều phiên họp nữa, với phiên bản thứ 18 dự kiến sẽ diễn ra tại Graz vào tháng 9 năm 2026.

Tony Hoare tại hội nghị VSTTE, Zurich, tháng 10 năm 2005

Ý tưởng ban đầu của Hoare cho Grand Challenge đã không thành công: ông đã hình dung ra một nỗ lực tập thể lớn do chính phủ tài trợ để giải quyết vấn đề phần mềm đã được xác minh, được mô phỏng theo (ví dụ) dự án Manhattan hoặc giải mã bộ gen người. Điều đó đã không xảy ra; các chính phủ đã không phản ứng ở quy mô đó. Tuy nhiên, nhiều dự án quy mô nhỏ hơn đã diễn ra, và uy tín của Hoare cũng như năng lượng của ông trong việc thúc đẩy ý tưởng này đã tạo ra một cú sốc buộc cộng đồng khoa học máy tính và công nghệ phần mềm phải dành sự quan tâm mới đến việc xác minh phần mềm và sản xuất trong những năm gần đây một loạt các công cụ xác minh chương trình mạnh mẽ – hầu hết trong số đó, một cách tự nhiên, đều dựa trên những ý tưởng quay trở lại bài báo về Ngữ nghĩa tiên đề năm 1969 của Hoare.

Dấu ấn của thời đại

Tôi thường nhận xét rằng cơ hội đáng kinh ngạc đối với một nhà khoa học máy tính hoạt động trong vài thập kỷ qua được tương tác với những người khổng lồ trong lĩnh vực này, như thể người ta đã gặp trong một đời (nhờ lịch sử ngắn gọn và cô đọng của lĩnh vực này) với những người tương đương với Archimedes, Descartes, Newton, Einstein và Planck. Hoare là một trong những người khổng lồ này, hoạt động trên nhiều mặt trận, xác định rất nhiều khái niệm quan trọng.

Tôi đã cố gắng đưa ra ý tưởng về nhà khoa học và nhà lãnh đạo, cũng như về con người. (Để xem trực tiếp, hãy xem Bài phỏng vấn Turing-Award-Series  của Cliff Jones.) Để kết luận, hãy để tôi sử dụng, thay vì từ ngữ, hai hình ảnh [34]. Một (lỗi, xin lỗi) là của Tony với vợ anh ấy là Jill, bản thân cô ấy là một lập trình viên, người luôn hiện diện mạnh mẽ trong cuộc đời anh ấy. Bức còn lại là của anh ấy ở sân bay Munich, sau khóa học hè ở Marktoberdorff, tôi nghĩ là vào tháng 8 năm 2004. Tôi có một chiếc ô tô thuê và đã chở anh ấy trở lại sân bay, rất vui khi nắm lấy cơ hội thảo luận dài về việc liệu Dijkstra, với thái độ của anh ấy đối với các bài kiểm tra được phản ánh trong một tuyên bố nổi tiếng, có bị ảnh hưởng bởi các cuộc thảo luận của Popper về vai trò của tính có thể chứng minh được trong khoa học hay không. Vì lý do nào đó mà anh ấy được tặng hai chiếc ô và vì lý do nào đó khác mà anh ấy có hai chiếc mũ. Chúng không vừa với hành lý của anh ấy. Tôi biết điều đó có vẻ vô nghĩa nhưng bằng cách nào đó người đại diện đã nói với anh ấy rằng anh ấy có thể mang theo mọi thứ lên máy bay. Cơ hội chụp được bức ảnh Tony đội mũ đôi và đội ô đôi (với hậu cảnh là cậu bé giật mình) là quá tốt để bỏ lỡ. Có rất nhiều nét về anh ấy trong bức ảnh chụp nhanh này: sự hài hước ẩn dưới sự nghiêm túc (hoặc có thể ngược lại), sự chấp nhận mọi thứ như hiện tại, tính thực tế và trần thế (tại sao lại từ bỏ bất kỳ tài sản nào của bạn?), sự pha trộn giữa sự nhút nhát rõ ràng và sự tự tin chắc chắn, sự sẵn sàng chịu đựng một chút ngớ ngẩn. Chúng tôi nhớ anh ấy.

Tài liệu tham khảo và ghi chú

1. C. A. R. Hoare: Quần áo cũ của Hoàng đế, trong Truyền thông của ACM, tập. 24, không. 2, trang 75–83, 1981, có tại https://dl.acm.org/doi /10.1145/358549.358561.
2. C.A.R. Hoare: Thủ tục và tham số: Cách tiếp cận tiên đề, trong Hội nghị chuyên đề về ngữ nghĩa của ngôn ngữ thuật toán, do E. Engeler biên tập, trang 102–116, Springer, 1971, có tại https://dl.acm.org/doi/10.5555/63445.C1104361.
3. C.A.R. Hoare: Quicksort, trong Tạp chí Máy tính, tập. 5, không. 1, trang 10–16, 1962, có tại https://www.cs.ox.ac.uk/files/6226/H2006%20-%20Historic%20Quicksort.pdf.
4. C.A.R. Hoare: Thuật toán 64: Quicksort, trong Truyền thông của ACM, tập. 4, không. 7, trang 321, 1961, có tại https://dl.acm.org/doi/10.1145/366622.366644.
5. Phiên bản Quicksort này đã được Leslie Lamport nhắc đến trong một video bài giảng nhưng ông chưa công bố. Gọi nó là “Lampsort”, tôi đã mô tả nó trong B. Meyer: Lampsort, bài viết blog trong blog Technology+, ngày 7 tháng 12 năm 2014, có tại https://bertrandmeyer.com/2014/12/07/lampsort/.
6. Alan Turing: Kiểm tra quy trình lớn, Báo cáo về Hội nghị về Máy tính toán tự động tốc độ cao, 67–69, 1949. Tốt nhất nên đọc khi được đưa vào, sửa chữa và thảo luận trong mục sau [7].
7. F. L. Morris và C. B. Jones: Chứng minh chương trình ban đầu của Alan Turing, trong Biên niên sử về lịch sử máy tính, tập. 6, không. 2, trang 139–143, 1984, có tại https://ieeexplore.ieee.org/document/5011915.
8. T. B. Steel (ed.): Ngôn ngữ mô tả hình thức Ngôn ngữ lập trình máy tính, North-Holland, 1966.
9. Robert W. Floyd: Gán ý nghĩa cho chương trình, trong Proc. Hội nghị chuyên đề của Hiệp hội Toán học Hoa Kỳ về Toán ứng dụng, tập. 19, trang 19–31, 1967, có tại https://link.springer.com/content/pdf/10.1007/978-94-011-1793-7_4.pdf.
10. C.A.R. Hoare: Cơ sở tiên đề cho lập trình máy tính, trong Communications of the ACM, 12(10), trang 576–580, 583, 1969, có tại https://dl.acm.org/doi/pdf/10.1145/363235.363259.
11. Krzysztof R. Apt: Mười năm logic của Hoare: Một cuộc khảo sát—Phần I, Khảo sát máy tính ACM, tập. 13, không. 3, trang 431–483, 1981, có tại https://dl.acm.org/doi/10.1145/356850.356855.
12. Krzysztof R. Apt: Mười năm logic của Hoare: Khảo sát—Phần II: Thuyết không xác định, Giao dịch ACM trên ngôn ngữ lập trình và hệ thống, tập. 6, không. 1, trang 1–39, 1984, có tại https://dl.acm.org/doi/10.1145/357233.357234.
13. C.A.R. Hoare: Bằng chứng về tính đúng đắn của việc biểu diễn dữ liệu, trong Acta Informatica, tập. 1, không. 4, trang 271–281, 1972, có tại https://link.springer.com/article/10.1007/BF00289507.
14. Các tài liệu tham khảo về Wirth, Boehm và Ichbiah là các siêu liên kết đến các cáo phó mà tôi đã viết cho mỗi người trong số họ.
15. Niklaus Wirth và C. A. R. Hoare: Đóng góp cho sự phát triển của ALGOL, trong Truyền thông của ACM, tập. 9, số 6, trang 413–432, 1966.
16. C. A. R. Hoare: Tham khảo không có giá trị: Sai lầm tỷ đô, QCon London, 2009, bản tóm tắt có tại https://www.infoq.com/pdfations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare/.
17. C. A. R. Hoare và Niklaus Wirth: Định nghĩa tiên đề về ngôn ngữ lập trình Pascal, Acta Informatica, tập. 2, không. 4, trang 335–355, 1973.
18. O.-J. Dahl, E. W. Dijkstra và C. A. R. Hoare: Lập trình có cấu trúc, Nhà xuất bản Học thuật, 1972.
19. C. A. R. Hoare: Giám sát: Khái niệm cấu trúc hệ điều hành, trong Truyền thông của ACM, tập. 17, không. 10, trang 549–557, 1974, có tại https://dl.acm.org/doi/10.1145/355620.361161.
20. C. A. R. Hoare: Giao tiếp các quy trình tuần tự, trong Truyền thông của ACM, tập. 21, không. 8, trang 666–677, 1978, có tại https://dl.acm.org/doi/10.1145/359576.359585.
21. Edsger W. Dijkstra: A Discipline of Programming, Prentice Hall, 1976. Cuốn sách này là sự sàng lọc và mở rộng bài viết trước đó của Dijkstra: Các lệnh được bảo vệ, tính không xác định và dẫn xuất chính thức của chương trình, trong Truyền thông của ACM, tập. 18, không. 8, trang 453–457, 1975, có tại https://dl.acm.org/doi/10.1145/360933.360975.
22. C. A. R. Hoare: Quy trình giao tiếp tuần tự, Prentice Hall, 1985.
23. A. W. Roscoe: Lý thuyết và thực hành về sự tương tranh, Prentice Hall, 1997, được tác giả cung cấp tại http://www.cs.ox.ac.uk/people/bill.roscoe/publications/68b.pdf.
24. Cliff B. Jones: Phát triển phần mềm: Một cách tiếp cận nghiêm ngặt, Prentice Hall, 1980. (Để tìm hiểu về VDM ngày nay, người ta nên sử dụng Phát triển phần mềm có hệ thống bằng VDM của Jones, Prentice Hall, 1990, bản thân nó đã có ấn bản đầu tiên vào năm 1986.)
25. J.-R. Abrial, S. A. Schuman và Bertrand Meyer: Ngôn ngữ đặc tả, trong Về xây dựng chương trình, do R. M. McKeag và A. M. Macnaghten, trang 343–410, Nhà xuất bản Đại học Cambridge, 1980, có tại https://se.inf.ethz.ch/~meyer/publications/laculars/Z_origen.pdf.
26. Tính hóm hỉnh của Goethe có lẽ ám chỉ đến bản dịch Faust của Gérard de Nerval sang tiếng Đức, bản dịch mà người ta cho rằng khi về già ông thích bản gốc hơn.
27. Jim Woodcock và Jim Davies: Sử dụng Z: Đặc tả, sàng lọc và chứng minh, Prentice Hall, 1996,
28. Cliff B. Jones: Các bước dự kiến hướng tới phương pháp phát triển để can thiệp vào các chương trình, trong Giao dịch ACM trên ngôn ngữ lập trình và hệ thống, tập. 5, không. 4, trang 596–619, 1983, có tại https://dl.acm.org/doi/10.1145/69575.69577.
29. A. W. Roscoe (biên tập viên): A Classical Mind: Các tiểu luận tôn vinh C. A. R. Hoare, Prentice Hall, 1994.
30. Cliff B. Jones, A. William Roscoe, và Kenneth R. Wood (biên tập viên): Suy ngẫm về công việc của C. A. R. Hoare, Springer, 2010.
31. Patrick Cousot và Radhia Cousot: Giải thích trừu tượng: mô hình mạng thống nhất để phân tích tĩnh các chương trình bằng cách xây dựng hoặc xấp xỉ các điểm cố định, trong POPL (Nguyên tắc ngôn ngữ lập trình), Thông báo ACM SIGPLAN, trang 238–252, 1977, có sẵn tại https://dl.acm.org/doi/10.1145/512950.512973.
32. C. A. R. Hoare và He Jifeng: Các lý thuyết thống nhất về lập trình, Prentice Hall, 1998.
33. Bertrand Meyer và Jim Woodcock (biên tập viên): Phần mềm đã được xác minh: Lý thuyết, Công cụ, Thí nghiệm, Hội nghị làm việc IFIP đầu tiên, VSTTE 2005, Zurich, Thụy Sĩ, ngày 10-13 tháng 10 năm 2005, Các bài thảo luận và bài báo chọn lọc đã sửa đổi, Ghi chú bài giảng về Khoa học máy tính, tập. 4171, Springer, 2008.
34. Từ “Thư viện các nhà khoa học máy tính” của tôi tại https://se.inf.ethz.ch/~meyer/gallery/.