June 11th, 2016

Gen.Turgidson

Задача о ферзях:

t(a,b,c){int d=0,e=a&~b&~c,f=1;if(a)for(f=0;d=(e-=d)&-e;f+=t(a-d,(b+d)*2,(
c+d)/2));return f;}main(q){scanf("%d",&q);printf("%d\n",t(~(~0<<q),0,0));}

Работает, кстати

PS: алгоритм реально красивый - я этого варианта не знал - подробное разъяснение тут (откуда собственно это и вытащил) - начиная с последнего абзаца второй страницы
Gen.Turgidson

Не прошло и 15 лет, как в голове сложилась картинка

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

SCADE - из INRIA уши растут, SPARK на ихнем движке работает, язычок F* на котором я примеры как раз приводил - сопродукция MS Research и INRIA (щас ушел полностью под INRIA), И кстати казавшийся мне странным их выбор проектов на деле совершенно логичен и даже довольно прикладного свойства.

Совершенно не удивлюсь если окажется что спонсируют все это EADS и Areva с лягушачьим министерством обороны на паях. Точнее довольно сильно удивлюсь если это не так.

И кстати особенности эволюции OCaml ясны - он под конкретные задачи на сам деле развивается

PS: Coq кстати тоже давно уже не только абстрактная формализация математики, а один из самых мощных движков под это дело (в принципе тот же why3 может и его использовать) - просто как я понимаю для end-user-овского продукта сложноват в использовании

Xavier Leroy кстати занимается щас compcert - полностью верифицированным компилятором С (сейчас утверждается, что на 90% примерно) - тоже когда первый раз узнал очень удивился - а сейчас все на свои места тоже стало
Gen.Turgidson

Мирное сияние чистого разума

Вот Воеводский и ко - Унивалентные основания математики - что казалось бы может быть оторванее от жизни и мирнее.

Собственно сам так думал - "Впрочем, теперь, когда сведения мои пополнились" (© "Сердце тьмы") я бы насторожился уже при фразе "идея использования интуиционистской теории типов Пера Мартин-Лёфа", после же упоминания "В феврале 2010 года Воеводский начал создавать библиотеку на Coq..." - у меня в голове начинает играть военная музыка :)))

Потом опять окажется что все это прибрало под себя министерство обороны с боингом и аэробусом :)))

Cобственно - иллюстрация к той старой истории в MIT AI Labs: http://kouzdra.livejournal.com/3007623.html

PS: Как там в фашистском Мюнхаузене:
https://youtu.be/w2It3PCRiUo?t=4753
Collapse )
Dr.Strangelove

Разговор ватника с креаклом

На сам деле очень забавное: главное - систематизирующее:
http://dysto.livejournal.com/489753.html?thread=4186649#t4186649

Там в общем все прекрасно (и главное - очень характерно) - но один тред выделю:

- - мне еще в школе сделали могучую прививку от креакловости - поместив соответствующую среду. Диагноз креаклитету (тогда называвшемуся "советской интеллигенцией") - крайне завышенная самооценка в сочетании с довольно-таки средненьким реальным уровнем.

PS: То есть с подменой реальных знаний и умений тусовочным духом и проч. В этом смысле кегебе и проч - куда более здоровые структуры - все-таки более или менее меритократические

...
- Я не в том положении нахожусь, чтобы вам рекомендовать посмотреть этот фильм, тем более что вы наверняка воспримете его примерно как один из донецких продавцов, когда я у него спросил про Апокалипсис Сегодня: "А, это там где вертолёты летят". И ведь правильно же формально :).

- Ну так он и прав. Красивая, но крайне невнятная "модернистская" экранизация "Сердца тьмы". Без которого там вообще imho ничего не понятно - а поскольку большинство поклонников этого фильма Конрада не читало - то и не понимает - выдумывая какую-то хрень вместо простого довольно смысла.

- Конрада не читал, так и есть.

Апокалипсис - фильм сам по себе ясный, как небо в летний полдень, даже если не знать, что, например, сам Коппола о нём говорил.
...
Коппола взял какой-то древний манускрипт, интересный только специалистам, и сделал на его основании великий фильм. Это обычная история, как говорит Гринуэй в начале "Данте" - "Хороший старый текст - прекрасное пространсто для импровизации".

- Коппола взял книжку, которая стандартно входит в любой практически топ-100 английской литературы, если что.

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

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

Но там все прекрасное.
Major Kong

Ватники vs креаклы

А кстати комментатор ненароком выдал видимо формулу отделяющую одних от других:
ОСНОВНАЯ СОВЕТСКАЯ ПИСЕЧКА вообще. Не надо быть каким-то юбер-профи, главное - быть хорошим человеком. На этом вообще вся советская ткань держалась.

Да, где-то там вдали за рекой были люди, ночующие у станков в ватниках, или сгоревшие на работе, Ленинская премия, Гертруда и похороны на лафете, но это было как в кино.

А на деле, на каждый день - "главное - быть хорошим человеком".


Ну да - у одних - на деле "как в кино", а другим важно "быть хорошим [совестливым] человеком".

Собственно к этому и сводится.

И кстати - как ни смешно - "Трудно быть богом" в этом смысле очень знаковая книжка - дон Румата очень сильно старается "быть хорошим человеком" - а потом его пробивает - и выходит - "как в кино".