Мягкое введение в Coq: начало

Тогда ждем следующих частей, спасибо.

Мягкое введение в Coq: начало

Формальное описание — это же и есть программа для Coq, верно? Если в формальном описании есть ошибки, то смысл верификации программы пропадает — но как гарантировать то, что их нет? Иными словами, кто будет проверять проверяющего? :)

Честно говоря, я пошел читать про формальную верификацию в Википедии и окончательно запутался в том, что же она, собственно, из себя представляет и как ее применить применительно к более «бытовым» сценариям. Вы не могли бы, например, в следующих статьях (или в комментариях, если ответ тривиален) показать, как именно можно верифицировать стандартный C-шный Hello World?

#include <stdio.h>

int main(int argc, char *argv[]) {
    printf("Hello, world!\n");
    
    return 0;
}

Мягкое введение в Coq: начало

А как верифицировать программы, написанные для Coq? Т.к. они пишутся людьми, в них же тоже возможны ошибки, которые нужно исключить?

Гипотеза Била подорожала до 1 миллиона долларов

Гугл о таких умниках уже подумал

Общественный совет при ФСБ предлагает запретить Tor и сайты-анонимизаторы, привлечь к ответственности их создателей

Запретить игровые сервера! Запретить покупку VDS без разрешения органов!

Обручальное кольцо светится, если взять за руку

Было бы кольцо 15.73, пришлось бы наращивать.

Общественный совет при ФСБ предлагает запретить Tor и сайты-анонимизаторы, привлечь к ответственности их создателей

А почему нет варианта «любое насильственное причисление к любому религиозному/политическому движению является злом без исключения»? А то, получается, есть либо христиане, либо представители других религий и конфессий, а разумные люди, выходит, вымерли.

Реализация стилей подчеркивания в LESS через генерацию png в data-URI

Firefox 21 — к сожалению, не совсем работает:

(большая версия по клику)

Архив интересного кода

Надеюсь, в коллекцию попадет референсная реализация bubblesort ;)

Поддержка The Neverhood добавлена в ScummVM

А разве ScummVM поддерживает исключительно SCUMM? :)

Как работает «Освободитель» (Да-да, мы напечатали пистолет)

Minecraft.

Как работает «Освободитель» (Да-да, мы напечатали пистолет)

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

Неизвестный математик совершил прорыв в теории простых чисел-близнецов

Largest even prime

Even

prime

Как работает «Освободитель» (Да-да, мы напечатали пистолет)

Какого ж размера должно быть шоколадное яйцо… хммм, а ведь это идея :)

Как работает «Освободитель» (Да-да, мы напечатали пистолет)

Ну я вот, например.

Как работает «Освободитель» (Да-да, мы напечатали пистолет)

Unbiased-рендереры и не такое умеют.

Скрытый текст

Skype просматривает содержимое ссылок отправленных в чате

И самым популярным советом на форумах вебмастеров в ответ на «Как бороться с DDoS-ом от Microsoft» будет «Отключите SSL, он все равно не нужен никому.».

Браво.

Вычисление N-го знака числа Пи без вычисления предыдущих

Ждем ASIC-ов.

Вычисление N-го знака числа Пи без вычисления предыдущих

Тогда правильно ли я понимаю, что время выполнения не зависит от основания системы счисления, даже если оно будет порядка (2**64)?

Если так, то можно значительно ускорить вычисления за счет VLIW/SIMD.

Вычисление N-го знака числа Пи без вычисления предыдущих

А чему соответствует C?