Кодеры за работой

Айк: Я много занимался физикой, прежде чем обратился к математике и компьютерным наукам. Я довольно много занимался математикой, получая через это знания по программированию, а также изучал кое-что самостоятельно и поэтому на занятиях сидел в задних рядах — скучал, ерзал, делал что-то свое. От этого сильно страдала самодисциплина, и я, вероятно, пропустил кое-что важное.

Разговаривая с теми, кто получил PhD, я понимал: кое-что они знают лучше меня. И я думал об упущенных возможностях, которых уже не вернуть. Можно освоить что-нибудь благодаря Интернету, но разве это заменит хорошего преподавателя и систематический курс обучения? Правда, я не очень жалею об этом.

Что касается программирования, то я всегда говорил, что занимаюсь низкоуровневым программированием. Объектно-ориентированное программирование, шаблоны проектирования — это не для меня. Я так и не купил книгу Эриха Гаммы. Кое-кто в Netscape потрясал этой книгой как Библией — наши с Джейми Завински враги-коллеги, пришедшие в компанию после ее покупки. Просто невыносимо, учитывая, что это были далеко не лучшие программисты.

Сложись все иначе, я мог бы заниматься и высокоуровневыми вещами. Думаю, работая в Mozilla и имея дело с Firefox, я узнал больше о разработке через тестирование — то был ценный опыт. Было и кое-что еще, например тестирование с использованием случайных данных, которого проводилось много. У нас было много исходных языков, были большие и глубокие конвейеры рендеринга, сильно подверженные ошибкам, связанным с безопасностью доступа к памяти. Вообще, тестирование с использованием случайных данных оказалось самым продуктивным видом тестирования.

Я также стоял за увеличение вложений в статический анализ, и это оказалось правильным, хотя сама по себе штука довольно темная. Но мы наняли тех, кто хорошо в нем разбирался.

Сейбел:

Статический анализ какого именно вида?

Айк: Анализ языка C++, выполнить который непросто. Обычно при статическом анализе вы анализируете программу целиком и стремитесь, скажем, доказать корректность состояния памяти. Нужно устранить все неоднозначности, а для этого найти в памяти все альтернативные имена — это проблема экспоненциального характера, обычно нерешае-мая ни для одной более-менее крупной программы. Большой прорыв, однако, заключался в том, что больше не надо было волноваться насчет памяти. Если построить полную диаграмму исполнения команд и связать воедино все виртуальные методы с их возможными реализациями, то можно частично оценивать код, не запуская его. Можно найти недостижимый код, можно найти избыточные проверки и пропущенные проверки на NULL.

Можно сделать еще больше на высших уровнях, где работаешь, когда в голове есть система доказательств для программы, которую пишешь. Но в обычных языках нет системы типизации для выражения терминов доказательства. И это серьезная проблема. Согласно Карри-Говарду, существует зависимость между логическими системами и системами типизации, типы являются термами, а программы — доказательствами, и поэтому в принципе можно описать высокоуровневую модель, которую намереваешься создать. Например, такой-то массив на раннем этапе должен иметь ограничение по длине, а на прочих этапах имеет другие ограничения — или не имеет их вовсе. Хитрость отчасти и состоит в том, что на разных этапах действуют разные правила. Или, например, вы надежно защищены внутри своей абстракции и ради большей эффективности нарушаете собственные инварианты — но при этом знаете, что делаете, и знаете, что с внешней точки зрения вы в порядке. Все это очень трудно реализовать в программах с жесткой проверкой типов.

Когда пишешь программу на языке Haskell, приходится выбрать систему доказательств еще до того, как толком поймешь, что именно делаешь. Динамические языки стали популярными, поскольку человек может быстро создать прототипы и держать в голове потенциальную систему типизации. А уже потом, если язык поддерживает это свойство или при перекодировании в статический язык, можно создавать типы. Это одна из причин того, почему мы были заинтересованы в наличии необязательной типизации в JavaScript. Мы заинтересованы в этом до сих пор, хотя среди руководства есть разногласия. Есть неплохие шансы на то, что в будущей версии JavaScript мы получим какую-нибудь смешанную систему типизации.

Поэтому мы хотим снабдить наш C++ аннотациями, на которые можно опираться при консервативном статическом анализе. Именно при консервативном, когда программа не зависает, до бесконечности пытаясь решить проблему экспоненциального свойства. Это поможет нам с проверкой безопасности сборщика мусора или с разделением функций на те, которые получают управление из скриптов, и те, которые передают управление скриптам, или с восстановлением стека интерпретатора, чтобы выносить заключение о безопасности. Мы получим параметры безопасности, которые сможем проверять. Многие из них — это высокоуровневые параметры и относятся не только к безопасности памяти. Поэтому мы должны продолжать борьбу на этом поле.