Это немного расплывчатый вопрос, но я пойду.
Гетерогенные среды
Задача сериализации состоит в том, чтобы взять данные в памяти одной компьютерной программы, преобразовать их в какое-то стандартизированное представление и преобразовать их обратно в данные в памяти другой компьютерной программы на совершенно другом компьютере. , Это открывает некоторые интересные возможности.
Например, представлением значения с плавающей запятой на многих компьютерах является IEEE754. Но это не совсем универсально; Исторически такие компании, как Cray и IBM, использовали альтернативные форматы, и поэтому существует вероятность того, что значение при десериализации на этих машинах может не совпадать со значением, которое было изначально сериализовано. Обычно это никого не волнует, потому что различия очень малы.
Это проявляется в некоторых технологиях сериализации; Собственные проводные форматы ASN.1 для чисел с плавающей запятой - это либо текстовое представление, либо его собственный двоичный формат, который не является IEEE754. Идея текстового представления заключается в том, что оно может передавать любое значение с плавающей запятой без ограничений. Напротив, двоичный формат часто имеет ограничения в точности, максимальном значении и т. Д.
Текст - еще одна потенциальная проблемная область; Сериализованные строки Unicode, отправленные на другой компьютер, который не поддерживает Unicode, могут привести к тому, что десериализованная строка будет отличаться от оригинала.
Аналогично с платформами, которые не поддерживают 64-битные целые числа и т. Д. Java очень раздражает - исторически у нее не было целых чисел без знака, поэтому обработка 64-битных значений без знака, полученных, скажем, от программы на C ++, является неприятностью.
Вывод - это логическая невозможность
Таким образом, в некоторых смыслах для гетерогенных сред не может быть официально доказано, что технологии сериализации воспроизводят идентичные значения, потому что машина назначения имеет другую архитектуру, и ее представление может быть иным или каким-то образом ограниченным.
Гомогенная среда
Сериализация, используемая для передачи данных из компьютерной программы на одном компьютере в точно такую же программу на идентичном компьютере (то есть в однородной среде), должна давать точно такие же значения при десериализации. AFAIK нет официально проверенных технологий сериализации. Если в язык Ada встроена сериализация (я не знаю), то компилятор Greenaills Ada формально доказан. Boost для C ++ тщательно проверяется коллегами, поэтому он подходит ближе, особенно если он используется поверх формально проверенного компилятора C ++ Greenhill и имеет библиотеку сериализации. Некоторые из коммерческих инструментов / библиотек ASN.1 очень развиты и пользуются большим доверием.
Что это официально доказано?
В этом последнем абзаце я затронул проблему с вашим вопросом; формальное доказательство, возможно, имеет смысл только в том случае, если весь стек разработки программного обеспечения (библиотеки, компилятор, ЦП) и исходный код приложения сами формально доказаны. В противном случае у вас мог бы быть идеальный исходный код для библиотеки сериализации, компилируемой нежелательным компилятором, связанной с мусорными библиотеками, работающими на неуклюжем процессоре; это не сработает.
Итак, когда кто-то говорит о «формально доказанном», он обычно говорит о всей системе, а не только об отдельном компоненте. Компонент, который сам по себе формально доказал, что соответствует его спецификации, является хорошим помощником в создании проверенной системы, но он волшебным образом не придает «правильности» всей системе в одиночку. Каждый другой компонент также должен соответствовать его спецификации.
И то, что мы видели исторически, это то, что довольно часто ЦП на самом деле не делают того, о чем говорится в их листе данных. Некоторые из них будут использовать ярлыки в арифметике с плавающей запятой в интересах выполнения инструкций за один цикл, а не для достижения идеального результата.
Извините за бессвязный ответ, но я надеюсь, что это будет интересно и поможет.