История изменений

Как из того, что не компилируются два частных случаях, следует, что возможна верификация в общем?

Про в общем никто не говорил. Речь была про «эти функции (kmalloc) нельзя вызывать из этих функций (обработчики прерываний)» что я назвал моделью и верификацией по ней. (Нам бы определённых артиклей сюда).

Огромный класс программ (наверное, даже большинство программ) _|_ by design

Например? Термы EventLoop : Type не есть то что населяет _|_, термы бесконечного Stream : Type -> Type — тоже.

Ты наверно думаешь, что non-termination обязательно населяет _|_? Необязательно.

А нам это и надо.

Если надо, то используем контейнеры IO. Если зачем-то надо (хотя перекинуть значение между каналами без thread-safety это что-то специальное) STM трогать не атомарно, то достаём по atomically read-from-chan, обрабатываем f и пишем с помощью atomically write-to-chan, то есть write-to-chan-io a =<< f <$> read-from-chan-io b.

На самом деле, эта функция может делать что угодно.

Баг в реализации языка? Зачем сводить всё к абсурду? Доказательства математических фактов и свойств программ вообще на агде вполне правильны, постольку-поскольку.

А кто докажет, что твое доказательство будет правильным?

А, вопросов нет. Непротиворечивость ZFC или PA (trolling intended) тебе никто не докажет.

При чем тут тогда статика неясно вовсе.

dmfd рассказывал про случай когда фабрика генерирует недетерминированным образом значения типов A, B, C, ..., то есть либо вариант, либо T, а другой потребитель даункастит это к конкретному A — падение не наступает при запуске программы, как ты говоришь, а лишь тогда когда фабрика соберёт значение по отношению к которому потребитель частичен. Статика тут станет ещё не просто статическими проверками против даункастов, но и инструментом разработки/рефакторинга — утверждение A + B + C + ... для фабрики вынудит потребителей покрывать все ветви, а при изменении типа фабрики потребуется привести в порядок всех её потребителей.

Ясно, нет?

Да, просто это звучит, с точность до дуальностей, как «зависимое произведение это не произведение» (там pullback, то есть co-pushout, как обобщение product, то есть co-sum).

Нам нужно писать программы с _|_

Тебе нужно писать абсурдные программы? Зачем? :)

Как из того, что не компилируются два частных случаях, следует, что возможна верификация в общем?

Про в общем никто не говорил. Речь была про «эти функции (kmalloc) нельзя вызывать из этих функций (обработчики прерываний)» что я назвал моделью и верификацией по ней. (Нам бы определённых артиклей сюда).

Огромный класс программ (наверное, даже большинство программ) _|_ by design

Например? Термы EventLoop : Type не есть то что населяет _|_, термы бесконечного Stream : Type -> Type — тоже.

Ты наверно думаешь, что non-termination обязательно населяет _|_? Необязательно.

А нам это и надо.

Если надо, то используем контейнеры IO. Если зачем-то надо (хотя перекинуть значение между каналами без thread-safety это что-то специальное) STM трогать не атомарно, то достаём по atomically read-from-chan, обрабатываем f и пишем с помощью atomically write-to-chan, то есть write-to-chan-io a =<< f <$> read-from-chan-io b.

На самом деле, эта функция может делать что угодно.

Баг в реализации языка? Зачем сводить всё к абсурду? Доказательства математических фактов и свойств программ вообще на агде вполне правильны, постольку-поскольку.

А кто докажет, что твое доказательство будет правильным?

А, вопросов нет. Непротиворечивость ZFC или PA (trolling intended) тебе никто не докажет.

При чем тут тогда статика неясно вовсе.

dmfd рассказывал про случай когда фабрика генерирует недетерминированным образом значения типов A, B, C, ..., то есть либо вариант, либо T, а другой потребитель даункастит это к конкретному A — падение не наступает при запуске программы, как ты говоришь, а лишь тогда когда фабрика соберёт значение по отношению к которому потребитель частичен. Статика тут станет ещё не просто статическими проверками против даункастов, но и инструментом разработки/рефакторинга — утверждение A + B + C + ... для фабрики вынудит потребителей покрывать все ветви, а при изменении типа фабрики потребуется привести в порядок всех её потребителей.

Ясно, нет?

Да, просто это звучит, с точность до дуальностей, как «зависимое произведение это не произведение» (там pullback, то есть co-pushout, как обобщение product, то есть co-product).

Нам нужно писать программы с _|_

Тебе нужно писать абсурдные программы? Зачем? :)