Вопрос к дебианщикам: есть неизвратный способ запускать несколько instance'ов MariaDB под Debian? Неизвратный == без создания 100500 init-скриптов и более/менее нормально вписывающийся в существующую систему debian-скриптов.

Вопрос достаточно важный, потому рекоменд приветствуется.

О, очередной пылкий вьюноша со «скобочным вебом»!

Ну, попробуй реализуй скобочный веб, чо. Только сперва тебе придется написать свой валидирующий pull-парсер для S-выражений. Стандартный лисповый ридер не вернет AST, пока не распарсит все до последней скобки, а в вебе надо начинать интерпретировать по возможности сразу же.

Затем ты напишешь разборщик и валидатор своих DSL-аналогов HTML и CSS и начнешь реализовывать рендерер. В этот момент обнаружится, что для лиспа нет качественных биндингов к современным GUI-тулкитам. Сперва ты возьмешься за cffi-cairo и cl-cairo2, но выяснится, что они заточены под старые версии Cairo и не работают.

Ты станешь допиливать Cairo-биндинги, но однажды решишь, что Cairo семантически чужд лисп-парадигме и возьмешься писать свою кросс-платформенную библиотеку для поддержки высокопроизводительной векторной графики. Затем ты реализуешь аналог протокола HTTP, только на S-выражениях (назовем его SXTP), потому что HTTP с его убогими URL'ами и методами семантически чужд лисп-парадигме.

После этого встанет вопрос о написании веб-сервера, поддерживающего SXTP. Попутно ты напишешь template engine, аналоги XPath, XSLT, а также ORM и MVC-фреймворк. В этот момент выяснится, что традиционные SQL-базы данных семантически чужды лисп-парадигме, и ты начнешь разрабатывать собственную лисп-ориентированную БД.

В этот момент ты поймешь, что Common Lisp перегружен и недостаточно выразителен, его стандарт раздут, а макросы негигиеничны; что Scheme слишком минималистична и академична; что остальные диалекты лиспа либо маргинальны, либо требуют .NET/JVM. Тут тебе в голову придет идея создать собственный лисп. Ты потратишь несколько лет на разработку стандарта, реализацию языка и переписывание всего вышеперечисленного на твоем новом языке. После этого окажется, что все ужасно тормозит. И это, разумеется, исключительно по той причине, что операционные системы стандарта POSIX семантически чужды лисп-парадигме. Ты начнешь разрабатывать LISP OS.

В процессе разработки выяснится, что эффективная LISP OS для x86/ARM/MIPS не может быть создана в принципе, так как их семантика чужда лисп-парадигме. Ты возьмешься за изучение System C, Verilog, VHDL и в один прекрасный день создашь лисп-машину на FPGA.

В этот момент мозаика чудесным образом сложится. У тебя будут лисп-машина, лисп-OS, лисп-сервер и лисп-браузер. Ты восторженно оглянешься вокруг, и обнаружишь, что половина человечества уже переселилась на Gliese 581, а оставшаяся половина забыла про HTML/CSS/etc., как про страшный сон, и давно пользуется квантовыми компьютерами и квантовыми сетями. Но все это уже будет не важно. У тебя ведь будет лисп-браузер и полноценная замена HTML/CSS на S-выражениях.

Да и жить тебе останется не так и долго, потому что к этому моменту ты уже будешь дряхлым стариком.

Роберт Харпер в CMU проводит семинар по Homotopy Type Theory (HoTT, homotopytypetheory.org ) — cs.cmu.edu [15-819 Advanced Topics in Programming Languages, Fall 2013]

Утверждается, что курс self-contained, в доп.литературу вынесено только "Programming in Martin-Löf's Type Theory" [ cse.chalmers.se ]

Имеются также и видеозаписи с Харпером у доски, но там "Silverlight is required to use the Panopto viewer". Худо-бедно показывает, mp4 ничего не мешает выдернуть со страницы.

Определение: из двух математических объектов красивее тот, у которого больше группа автоморфизмов. А если группы автоморфизмов одинаковой мощности, то красивее тот, у которого группа автоморфизмов красивее.

Задача 1: Привести пример двух математических объектов неодинаковой красоты с несчётными группами автоморфизмов.

Задача 2: Привести пример двух математических объектов, сравнить красоту которых вручную нельзя, а не вручную NP-сложно.

Dream Theater — Overture 1928, исполненный на двух акустических гитарах двумя мастерами пальцевой техники игры: youtube.com
Энтузиазм и энергия так и прут и выливаются из экрана во внешний мир!
P.S. Если верить описанию, это у них на видео запечатлён первый подход.