Когда говорят о "бурбакизме" всегда вспоминается Арнольд с его остроумной критикой аксиоматического преподавания математики в школе.

Непогрешимость логистики

Что касается плодотворности, то Кутюра, по-видимому, строит наивные иллюзии. Логистика, по его мнению, дает изобретательности в ее распоряжение «леса и крылья». А на следующей, странице он говорит: «десять лет тому назад Пеано опубликовал первое издание своего «Formulaire» (2).

Как, уже десять лет, как вы имеете крылья, и вы еще не полетели!

Я питаю величайшее уважение к Пеано, который сделал превосходные работы (например, его кривая, которая заполняет целую площадь), но в конце концов он не ушел ни дальше, ни выше, ни быстрее, чем большая часть бескрылых математиков, и этот путь он мог бы ведь проделать так же хорошо на своих ногах.

Я, напротив, вижу в логистике только помеху для изобретателя; с ее помощью мы отнюдь не выигрываем в сжатости; если нужны 27 уравнений, для того чтобы установить, что 1 есть число, то сколько нужно будет уравнений, чтобы доказать настоящую теорему? Если мы различаем вместе с Уайтхедом индивид х, класс, единственный член коего есть х и который называется ix, затем — класс, единственный член которого есть класс с единственным членом x и который называется iix, то можно ли думать, что эти различия, как бы ни были они полезны, облегчат нам движение вперед?

Первая программа очень проста, сама строка Hello, world! составляет почти половину программы. Все что нужно сделать - это поместить в регистр AH номер функции DOS (9), адрес строки поместить в DS:DX и вызвать 21-е прерывание (символ доллара является концом строки):

  Адрес   Код        Метка   Команда
  -----   --------   -----   ------------------
  0100    1E                 push    DS
  0101    B4 09              mov     AH,09
  0103    BA 10 01           mov     DX,offset @H
  0106    0E                 push    CS
  0107    1F                 pop     DS
  0108    CD 21              int     21H
  010A    1F                 pop     DS
  010B    B8 00 4C           mov     AX,4C00H
  010E    CD 21              int     21H
  0110    48         @H:     db     "Hello, world!$"
  0111    65
  0112    6C
  0113    6C
  0114    6F
  0115    2C
  0116    20
  0117    77
  0118    6F
  0119    72
  011A    6C
  011B    64
  011C    21
  011D    24

Я бы сказал, что ассемблер вообще не для алгоритмов нужен...

Но фундаментальная слабость бурбакизма в том, что он изгоняет интуицию. Которая в конечном счете больше формалистики

ассемблер вообще не для алгоритмов нужен...

Это и есть формальный аксиоматический метод

Есть неизменная основа. ARM, x86 и иже. Кои разные. Но основополагающиe. А все теории суть построение непротиворечивых теорий. Кои могут быть любыми

как определить непротиворечивость для ARM, x86 и иже?

по мне, в любом случае должны признать любую последовательность команд работающей и никакого "противоречия" не может быть, поскольку таковые попросту не имеют смысла по отношению к ассемблерным последовательностям/программам

дойдя до своего конца, последовательность ассемблерных команд может остановиться, но может и НЕ остановиться никогда угодив в бесконечный (мото)цикл-цикл-цикл

Программа "не работает", если она вызывает например exception. Это явно не то, что задумывалось. Т.е имеем противоречие.

Противоречивость наступает тогда, когда очередная инструкция портит задуманную последовательность... вызовет ли очередная инструкция фатальный сбой или нет.

укладываем новое допущение поверх теории и смотрим - обрушит оно ее или ляжет нормально (А если ляжет, то обрушит ли теорию отрицание оного.)

думаю, что это немного другое, а не противоречие: программа делает нечто другое, что не дует нам в паруса; именно такого очень трудно избежать в компьютерных доказательствах 4-х красок и упаковки пространства шарами/ядрами.

не можем задумать наперёд "задуманную" последовательность или вызвать (или нет) "фатальный" збой, поскольку выполнение формальной последовательностью сугубо неформальных намерений (разработчика или заказчика) суть сугубо неформальная проблема и доказательству не подвержена.

если обрушит отрицание оного, то значит укладывать поверх якобы "новое" не стоило, поскольку оное уже было где-то пониже, может и поверху

не вижу пока как могут подвернуться нелегальные последовательности легальных ассемблерных команд

Хайдук wrote: Непротиворечивость определяется не для самих команд, а для теорий программ, созданных на их базе.
Очень просто определяется... Работает, или нет

Наборы же команд суть термы и схемы (ну не совсем конечно ) в метаматематическом смысле

Как сейчас помню, что на устройство ЕС 9024 из Крыма (или Одессы) пришло рацпредложение, которое устраняло неисправность, обнаруженную только после того как было выпущено около полутора десятков тысяч изделий: при перфорировании нескольких подряд повторяющихся групп из трех цифр происходил сбой (с вероятностью около 50%)

на последовательность команд, что ломает комп и превращает того в кирпич, можно смотреть как на останавливающуюся в смысле Тьюринга программу, в то время как операционная система есть пример обратного, бесконечно зацикленной программы ждущей следующего задания или (на телефоне, как я щас) ввода пальцами юзверей.

как всё время новые third-party apps всплывают