Details

The nature of computer programs can be characterized from two different viewpoints: as executable artifacts that create signals on a computing device or as pure mathematical objects with a rigorous, unambiguous semantics. To distinguish both usages I use the word “code” for the first and “program” for the second. This distinction is relevant to avoid confusion when discussing notions such as validity or correctness of software. The point is illustrated by refuting a well-known claim on the impossibility of verification and misleading claims about commercial products. At the same time the distinction “program versus code” is insufficient: I show that a “program” is always accompanied by an implicit or explicit application context which is necessary to scope its semantics. Ultimately, the analysis performed in this paper helps to distinguish relative from mathematical truths when discussing qualities of software.

Природа компьютерных программ может быть охарактеризована с двух разных точек зрения: как исполняемые артефакты, создающие сигналы на вычислительном устройстве, или как чисто математические объекты со строгой, однозначной семантикой. Чтобы различать оба употребления, я использую слово “код” для первого и “программа” для второго. Это различие уместно, чтобы избежать путаницы при обсуждении таких понятий, как достоверность или правильность программного обеспечения. Данный момент иллюстрируется опровержением известного утверждения о невозможности верификации и вводящих в заблуждение утверждений о коммерческих продуктах. В то же время разграничения “программа против кода ” недостаточно: я показываю, что “программа” всегда сопровождается неявным или явным контекстом приложения, который необходим для охвата ее семантики. В конечном счете, анализ, проведенный в этой статье, помогает отличить относительные от математических истин при обсуждении качеств программного обеспечения.

• Program and Code
  • THE TWOFOLD NATURE OF COMPUTER PROGRAMS
  • MATHEMATICAL PROOFS OF PROGRAM CORRECTNESS
  • PROGRAM VERSUS CODE:THE CASE OF FORMAL VERIFICATION
  • THE APPLICATION CONTEXT
  • RELATIVISM
  • CONCLUDING REMARKS
  • REFERENCES

Technology and Language: interdisciplinary open-access scientific journal = Технологии в инфосфере : междисциплинарный научный журнал открытого доступа / Санкт-Петербургский политехнический университет Петра Великого. — Санкт-Петербург: СПбПУ, 2020-. — Периодичность: 4 раза в год. — Выходит с 2020 г. — Загл. с титул. экрана. — Свободный доступ из сети Интернет (чтение, печать, копирование). — Электрон. журнал. — Текст: электронный

Technology and Language: interdisciplinary open-access scientific journal = Технологии в инфосфере : междисциплинарный научный журнал открытого доступа / Санкт-Петербургский политехнический университет Петра Великого. — Санкт-Петербург: СПбПУ, 2020-. Т. 3, № 2, 2022. — 1 файл (7,75 Мб). — Свободный доступ из сети Интернет (чтение, печать, копирование). — Электрон. журнал. — <URL:http://elib.spbstu.ru/dl/2/j24-479.pdf>.