Category: литература

Category was added automatically. Read all entries about "литература".

Опыт использования Coq на практике, или Как я сам себя отпетушил COQОКОКОКО

Есть время собирать опыт.

Есть время разбрасывать на вентилятор.




Уже довольно давно система типизации в окамле кажется мне слегка недостаточной.
Collapse )

По итогу -- впечатления смешанные.

coq, zgtz

Решил вспомнить молодость и подоказывать кое-что. У известного Адама взял какой-то пример, который он доказывает через свою придуманную для книги CPDT тактику "crush", но мне это не нравится. Хотя бы тем, что тактики не нравятся. Я хочу что-то более приближённое к конструктивному построению доказательства.
Итак, "ноль не больше нуля" с моим тупым доказательством через классические тактики.
Lemma zgtz : 0 > 0 -> False.
intro H. inversion H.
Qed.
Print zgtz.

На что генерится какой-то совершенно дебильный код:
Collapse )
Конечно, должен быть способ как-то более прямым образом это доказать.
Если есть идеи, куда копать -- подскажите.

C++ to C++ bindings

upd2, final
"Папа просил передать вам всем, что цирк закрывается. Нас всех тошнит."
Для объекта obj с полем field должно быть так, что присвоение нового значения (obj->field = new_value) в одном рантайме должно вызывать изменение значения obj->field в другом. Учитывая, что код для доступа к obj->field (который нечто вроде *(this+offset)) уже зафиксирован в библиотеке, и поменять его невозможно, получаем, что требуется совпадение раскладки полей в памяти. Так как я его не могу гарантировать, то вся затея лишается смысла.

для истории:

И смех, и грех, и ёбаный стыд, и блядский C++. Нужно из одного плюсового компилятора использовать плюсовую библиотеку, созданную другим компилятором.

По заверениям знающих, напрямую это не получится, потому что даже в случае одинакового компилятора, но при разных рантаймах начинается такое ололо, что проще застрелиться.

В качестве предположений имеем немало: допустим, нам известно, что базовые типы (всё, что проще классов и структур) совместимы на уровне abi, у нас есть полный список классов, методов и все их типы, и проблемы начинаются в классах, методах и исключениях. (шаблоны не беру, так как вроде мне они не нужны, да и не знаю, как их рассматривать вообще)

От вас же хочется критики. Как про концепции, так и про мелкие подробности.

Collapse )

А вот теперь мне стоит подумать над следующими вещами: получится ли? Правильно ли получится? Хочу ли я этого?

upd1/
FAIL. Если либа или создаёт, или возвращает объекты -- каждый возвращённый объект создавать во враппере? А если надо будет передать объект, который создался в проге, в либу?
/me ушёл думать дальше.

(no subject)

Дочитал книгу "Сказки тёмного леса" про приключения коллектива "Грибные эльфы".
shroom elf
Это просто охуительно! Ребята умеют жить на полную. Ржал аки конь. Пожалуй, самая весёлая книжка за последнее время.
В книге изложены весёлые истории, проделываемые над унылым говном, которое заворачивается в занавески, носит лосины и держит в лапках пластмассовые мечи -- над нашими маленькими забавными ролевиками.
Из книжки позаимствовал: 1. желание жить не слишком скучно, 2. рецепт напитка "Элберетовка" (варится на спирту, крепость на выходе порядка 70 градусов, останавливает необходимость скороварки), 3. рецепт напитка "Болгарский Чёрный" (портер "балтика 6" и спирт в пропорции 1:1), 4. слово "неуподоблюсь" (существительное) и выражение "список неуподоблюсь", 5. ёмкое слово "перекидываться" (если кратко -- резкое изменение психического состояния при определённых обстоятельствах), 6. игру в шышки (простая логическая игра).
Книжка подтвердила моё давнее убеждение, что всякой атсральной хуетой можно из человека сделать дебила (стр. 60..66, если чо).
Посмеялся над историями с участием некой "княжны". Я давно замечал тупость сей дамы, но теперь мне понятны корни тупости. Можно было бы её, болезную, пожалеть, если бы не её "Magic School".
Заочно познакомился с некоторыми ролевыми деятелями, гнилыми мудаками и педерастами. А вот экологические эпизоды меня слабо впечатлили.
Нашёл следы пидошки: цитата из какой-то рпг-шной эхи, полузнакомая фамилия "кантор" и знакомая фамилия "куковлев".
Поискал в инете и понаходил немного подтверждений некоторым описанным в книге событиям, то есть, правда в книге есть. Другое дело, что некоторые события могут быть описаны со смещёнными акцентами. Впрочем, книгу можно спокойно воспринимать как худло, книга обладает художественной ценностью.
В будущем -- буду перечитывать.

(no subject)

Дошёл я до классики. "The Programmer's Stone". Относительно русский перевод — тутачки. Очень нравится. Всем, кто около погроммирования, советую прочитать всё.

А тем, кому ещё нравится пихология, рекомендую первую главу. Различие между двумя стилями мышления, имхо, лежит где-то рядом с "гуманитаризмом гойловного мозга", да и просто интересно.

А теперь — немножко говна на лопате. Цитирую:

книга Страуструпа (Stroustrup) описывает объектный подход и язык C++ -- праздник стиля, интуиции, структуры, глубины и творчества. Это тяжелая книга, описывающая сложный язык программирования, но она написана великим картостроителем в действии, у которого нет внутренней неразберихи относительно предмета.

"Я совсем не это имел ввиду!", какбэ оправдывается Бьярн:

Чмоке.

Таки шолом.

Пишу мало, но это нормально. Есть две истории, которые никак не могут закончиться, а до окончания что-либо писать неохота. Получится излишек моих эмоций, которые никому не нужны. Буду лучше соответствовать летописному стилю, краткому и лаконичному, пусть и с отсутствием мелких деталей. Потом будут два жырных поста: один про жену, другой про две киски (частично бритые, кстати; именно там, где их оперировали).

Сегодня, имея в излишке свободное время, почитал вред-ленту. Действительно, был вред -- убил время (насмерть). Самое то, что запало в душу -- это соление залупы by lj user sharlei (или как-то так). Хотя остальное тоже хорошо -- ведь это же я подбирал себе френдленту, а не какой-нибудь там.

Нопесал пару полуинтересных программ и наткнулся на тупик в моей библиотеке в/в, связанный с особенностями венды. С неприятными, нутрянными. Всё у неё через жопу.

Главная причина поста: сегодня в процессе разнородного гугления нашлось:
При запросе "define:ibota privet" гугельман оптимистично пишет: "Возможно, вы имели в виду: define:rabota privet".

Гугль вообще добрый.