egplife
egplife
CS oop philosophy fp logic В сумме: Моя модель программиской гетеросмешаннойиерархии: ULTIMATESUPRAATMABRAHMAN->SOPHISMS->PLATON->MATH->COMPLEXITYLEVELS->ГЕТЕРОГЕНКА->GODLYFIRES->METAPHYSICALQUALITY->PHILOSOPHY->SCIENCES->PHYSICS->QUANTUMMECHANICS->И ТОЛЬКО ТУТ УЖЕ OBJECT, а Java начинается всего лишь с OBJECT

OBJECT->FUNCTION
OBJECT->PROCESS

#philosophy #oop #fp #logic #cs #programming #science #moq #brahman #parabrahman #supra #ultimate #ultimateartifact #artifact #metaphilosophy #java
Strephil
Strephil
CS github.com
andrew.cmu.edu

Сделали C-подобный язык с верификацией корректности с упором на многопоточность. Пишешь спецификацию, пишешь реализацию, доказательство генерируется само. Вдруг ты какой мьютекс не отпустили.
qnikst
qnikst
programming books CS Буду и сюда постить "хорошие статьи/книги" по понедельникам.

При программировании в языках с неизменяемыми структурами данных, часто применяются методы работающие со структурой в-целом. Такие техники позволяют писать программу, как объединение более простых подпрограмм. Однако этот подход может ухудшать производительность, т.к. заставяет создавать огромные структуры данных, для решения это проблемы используется оптимизации deforestation (и fusion), основанная на правилах перезаписи выражений. При этой оптимизации удаляются промежуточные структуры и при компиляции код обрабатывающий сложную структуру превращается в настолько же эффективный, как код написанный на С, но при этом более поддерживаемый. В диссертации Дункана Котса рассматриваются различные такие правила (со ссылками на статьи о них), а так же дается доказательство корректности, и минимальные требования к языку, в котором эффективно принимать данные правила.

D. Coutts, “Stream Fusion: Practical shortcut fusion for coinductive sequence types,” 2010.
qnikst
qnikst
CS typefun dependent-types И в догонку, допустим у меня есть линейный вектор, и я его сортирую; достаточно ли привести доказательства, что результирующая линейный вектор имеет тот же размер и сортирован.
Т.Е. Можно ли фактом использования линейных структур заменить доказательство того что новый вектор это перестановка элементов исходного?
qnikst
qnikst
CS learning Вот есть люди, которые в Chalmers пилят всякие инетерсные штуки типа линейных типов.
А почему если заходить на сайт и смотреть какие есть программы для Post Doc то там какая-то туфта :(
qnikst
qnikst
? CS ненужный_пост чистил Downloads, нашёл кучу классных книжек, не могу правда вспомнить в каком контексте я их скачивал и зачем оно было надо.
Вот нафига мне было:
Naming and synchronization in a decentralized computer system, 78 года и стоит ли её читать.
ndtimofeev
ndtimofeev
IT CS А где почитать почему сейчас все пытаются делать mark-and-move вместо mark-and-sweep? Ну то есть основные достоинства перемещающего сборщика мусора мне понятны, но в целом концепция выглядит контринтуитивно. Ганс Боём например всячески защишает mark-and-sweep.
4DA
4DA
CS SPb О, годнота в cs-клубе:

1. Семинар по параметризованным алгоритмам.
2. Вычислительная геометрия.
3. Параллельное программирование.
4. Суффиксные деревья: новые идеи и открытые проблемы.
5. Визуализация графов.

compsciclub.ru

Сам хочу сходить посмотреть на вычислительную геометрию и если хватит времени на параллельное программирование.
any1?
4DA
4DA
programming quote LOL CS LOR Значит как оно в приложении к CS? Берется уже существующий язык, ну который дан, который успешен, который популярен. Ну, не знаю, пусть будет джава как конкретный пример. Мы вполне можем писать на джаве и иметь профит — но вот нам мало, по-этому мы берем какой-то формализм и описываем на нем джаву, весь ее стандарт, со всеми гофовскими паттернами и прочей хренью (но такого формализма нет, беда), причем полностью описываем, безо всяких там «подмножеств», понятное дело. Потом смотрим, и внезапно оказывается, что язык удовлетворяет какому-то свойству Х, которого мы не ожидали! И, оказывается, на нем можно делать какое-то Y, которое мы, читая стандарт языка, и не думали, что можно! Вот это и называется практическим результатом.

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

linux.org.ru
skobkin-ru
skobkin-ru
игры лол CS картинки Архангельск Дело было в 2007 году. Мой провайдер проводил чемпионат по Counter-Strike 1.6.
Я собрал команду из знакомых игроков зарегистрировал на сайте провайдера. Позже выяснилась проблема. Сайт писал мудак, который не осилил кодировки. Так мой одноклассник стал ебцемхами.
img-fotki.yandex.ru
dukkha
dukkha
CS math Одно из определений класса NP из книги "Классические и квантовые вычисления" (А. Китаев, А. Шень, М. Вялый):

Имеются два персонажа: король Arthur (Артур), умственные способности которого полиномиально ограничены, и волшебник Merlin (Мерлин), который интеллектуально всемогущ и знает правильные ответы на все вопросы. Король A интересуется некоторым свойством (например, "есть ли у графа гамильтонов цикл"), а волшебник M хочет, чтобы король признал наличие этого свойства (ну, скажем, граф стремится к званию гамильтонова и дал M взятку). A не доверяет своему волшебнику, зная его корыстолюбие, и хочет иметь возможность самостоятельно проверить предложенный M ответ.
Поэтому они действуют следующим образом. A и M оба смотрят на слово x, после чего M сообщает некоторую информацию (слово y), которая должна убедить A, что L(x)=1. Используя эту информацию, A проверяет убедительность аргументов M некоторым полиномиальным способом.
В этих терминах определение класса NP можно сформулировать так: свойство L принадлежит классу NP, если у Артура есть полиномиальный способ проверять убедительность доводов Мерлина, причем:
L(x)=1 => у M есть способ убедить A в этом;
L(x)=0 => как бы M ни изощрялся, A не поверит, что L(x)=1.
xorkrus
xorkrus
игры WOT CS OpenTTD мышли Неужели ВОТ стоит того, чтобы люди платили за танки и маскировки?
Неужели игры вообще стоят того, чтобы за них платили?
Говно говном же.
Кроме TTD\OTTD и NFSWM — ни одна игрушка меня не зацепила. И если за TTD я бы заплатил (будь она... посовременней), то NFSMW не на столько хороша. Просто достойна.
А все остальные кризисы фарсру и прочая муть с чернобылем — гавно.
masai
masai
CS math вейвлеты Набросал-таки статейку про вейвлеты → habrahabr.ru
Рассчитано на тех, кто совсем ничего про них не знает. Иногда, по-моему, я перегибал палку и совсем уж всё примитизировал. Вставлять какой-то код было лень, ограничился формулами.
Под конец я понял, что если излагать всё, что хочу сказать, то книжка получится, так что местами получилось скомкано и очень кратко. Надеюсь, идею передать удалось.
masai
masai
? CS math А кому-то вообще было бы интересно прочитать про то, как сжимаются изображения с помощью вейвлетов, с объяснениями «на пальцах» (на уровне понимания матриц и их умножения)? А то уже несколько раз объяснял разным людям.
partizan
partizan
games CS посмотрел я на cs:go, ну, контр-страйк, графика получще чем source, но мне не понравилось в нем то же что и в source — движения все какие-то суперплавные, как будто я управляю камерой с приклееным ко лбу пистолетом. и прицелиться никак, реально привык к крузису — по умолчанию стреляем типа навскидку, а если надо точнее — целимся. это же круто, ну.
или это соревновательная игра для задрачивания на точность-скорость и тут такое только мешает? эх, жду свой крузис!
masai
masai
CS math Проверь свою интуицию! ;) Пусть x = 0,7. Операция x ← 11x-7 не должна менять его значение. Но есть ошибки округления и представления чисел в ЭВМ. За сколько шагов накопленная ошибка для типа double превысит тысячу?