У Айлин за последний месяц большой прогресс. Месяц назад её словарный запас фактически исчерпывался словами «мам!», «пап!», «ам!» (есть), «бау» (животное), «бу» (так она назвала любимую куклу), «мау» (кошка) и «дададаааа!» (увидела детскую площадку и хочет туда). Недель пять назад появились «нянь!» (Настя), «кука» (кукла) и «би» (машина). В первые ( Read more... )

Как все тут знают, по соответствию Карри-Говарда интуиционистской логике высказываний (логике нулевого порядка) соотведствует просто-типизированное лямбда-исчисление с произведениями STLC ( Read more... )

Фирма Laundroid, которая обещала нам all-in-one-робота, который сразу делает с постиранным бельём всё, что нужно, увы, ожидаемо загнулась ( Read more... )

Оказывается, iRobot выпустили новый офигенский робопылесос Roomba S9+, традиционно с пылесосной станцией, успешно компенсирующей малый объем пылесборника. Ругают его пока за сыроватый софт, но это невпервой, за годик они всё починят и апдейты пришлют. А вот само устройство меня впечатлило (ценой, правда, тоже впечатлило - $1500). Они сдались и ( Read more... )

(По следам переписки в комментариях с daedmenВы заезжаете на обычное такое наземное парковочное место - 2.30м в ширину, 6м в длину, может вдоль дороги параллельно, может перпендикулярно с отдельным въездом, только вместо того что границы нарисованы на земле белой линией, границы физические - под автомобилем не асфальт, а гидроизолированная стальная ( Read more... )

Может кто помнит, я несколько раз, начиная с 2003 года писал про то, что вот бы были посудомоечные машины, у которы ящики не просто выдвигаются, но и поднимаются, чтобы их загружать на уровне стола ( Read more... )

SpaceX вообще молодцы, я с диким интересом слежу за разработкой двигателя Raptor и ракеты BFR ( Read more... )

(Ежегодный пост ( Read more... )

“Eine Menge ist eine Zusammenfassung bestimmter wohlunterschiedener Objekte unserer Anschauung ( Read more... )

В математике понятие “теория типов” развивается, и ещё непонятно в какой общности нужно будет давать определение. В контексте информатики теориями типов называют обобщения λ→ - просто типизированного лямбда-исчисления ( Read more... )