Сабж. На главной висит две новости про Go.

На новость не тянет, имхо, так что напишу здесь.

SWI-Prolog обновился до версии 7.1.0. Подробный список изменений можно найти тут.

Версия для Ъ:

• Lists are no longer represented as .(H,T). Instead, the list functor is now '$cons'(H, T). The empty list is still [], but this is not an atom. I.e., '[]' == [] fails.
• By default, double quoted «text» is mapped to an object of type string. This already raised some discussions.
• The system introduces `maps' as primary citizens. Maps are collections of key-value pairs, optionally typed. Maps are supported by read and write.
• Quoted atoms are no longer operators.
• Unquoted atoms may contain internal dots. E.g., a.b is an atom.
• functor() is valid syntax. It produces a term that is distinct from 'functor'. The `block' operator '()' to hack this syntax has been removed.
• The `block' operators [] and {} remain.

Доступны слайды и видеозаписи лекций некоего Conor McBride.

Dependently typed functional programming languages such as Agda are capable of expressing very precise types for data. When those data themselves encode types, we gain a powerful mechanism for abstracting generic operations over carefully circumscribed universes. This course will begin with a rapid depedently-typed programming primer in Agda, then explore techniques for and consequences of universe constructions. Of central importance are the “pattern functors” which determine the node structure of inductive and coinductive datatypes. We shall consider syntactic presentations of these functors (allowing operations as useful as symbolic differentiation), and relate them to the more uniform abstract notion of “container”. We shall expose the double-life containers lead as “interaction structures” describing systems of effects. Later, we step up to functors over universes, acquiring the power of inductive-recursive definitions, and we use that power to build universes of dependent types.

http://lambda-the-ultimate.org/node/4804

С 4 ноября 2013 года на курсере начнется сабжевый курс, который продлится 7 недель (пруф).

Содержание курса:

• Week 1: Review of Principles of Functional Programming: substitution model, for-expressions and how they relate to monads. Introduces a new implementation of for-expressions: random value generators. Shows how this can be used in randomized testing and gives an overview of ScalaCheck, a tool which implements this idea.
• Week 2: Functional programming and mutable state. What makes an object mutable? How this impacts the substitution model. Extended example: Digital circuit simulation.
• Week 3: Futures. Introduces futures as another monad, with for-expressions as concrete syntax. Shows how futures can be composed to avoid thread blocking. Discusses cross-thread error handling.
• Week 4: Reactive stream processing. Generalizing futures to reactive computations over streams. Stream operators.
• Week 5: Actors. Introduces the Actor Model, actors as encapsulated units of consistency, asynchronous message passing, discusses different message delivery semantics (at most once, at least once, exactly once) and eventual consistency.
• Week 6: Supervision. Introduces reification of failure, hierarchical failure handling, the Error Kernel pattern, lifecycle monitoring, discusses transient and persistent state.
• Week 7: Conversation Patterns. Discusses the management of conversational state between actors and patterns for flow control, routing of messages to pools of actors for resilience or load balancing, acknowledgement of reception to achieve reliable delivery.

Recommended Background:

You should have a background equivalent to someone who completed the course “Principles of Functional Programming”. We assume you know the fundamentals of functional programming and the Scala language.

А почему бы не разрешить корректорам вносить изменения в опросы?

Сейчас корректорам приходится совершать слишком много действий:

• прилетело уведомление;
• тыкаем «править» и видим, что редактировать можно только заголовок и теги;
• идем в корректорскую рассылку или пишем модератору в джаббер;
• ?????
• PROFIT!

Дискасс.

В этом году приз Programming Languages Software Award достался Coq.

!Ъ: тыц

Ъ:

The Coq proof assistant provides a rich environment for interactive development of machine-checked formal reasoning. Coq is having a profound impact on research on programming languages and systems, making it possible to extend foundational approaches to unprecedented levels of scale and confidence, and transfer them to realistic programming languages and tools. It has been widely adopted as a research tool by the programming language research community, as evidenced by the many papers at SIGPLAN conferences whose results have been developed and/or verified in Coq. It has also rapidly become one of the leading tools of choice for teaching the foundations of programming languages, with courses offered by many leading universities and a growing number of books emerging to support them. Last but not least, these successes have helped to spark a wave of widespread interest in dependent type theory, the richly expressive core logic on which Coq is based.

As a software system, Coq has been in continuous development for over 20 years, a truly impressive feat of sustained, research-driven engineering. The Coq team continues to develop the system, bringing significant improvements in expressiveness and usability with each new release.

In short, Coq is playing an essential role in our transition to a new era of formal assurance in mathematics, semantics, and program verification.

Некто Andrej Bauer закончил работу над сабжевой книгой.

http://homotopytypetheory.org/book/

Исходники книги распространяются на условиях лицензии Creative Commons Attribution-ShareAlike 3.0 Unported License.

Скачать сорцы без регистрации и смс можно тут.

Вышла публичная бета книжки Real World OCaml.

Книга содержит три большие раздела: «Language Concepts» (общее описание языка), «Tools and Techniques» (hashtables, работа с json и т.п.) и «The Runtime System» (FFI, GC).

Краткая суть: необходимо для каждого зарегистрированного пользователя устанавливать лимит на доступное дисковое пространство, которое будет циклически перезаписываться по достижению границы.

Более подробно: есть сервис, который предоставляет пользователям всякие разные плюшки, планируется добавить видеонаблюдение. Продажники хотят продавать не объем дискового пространства, доступный за определенную абонентскую плату, а глубину архива — три дня/неделя и т.п. В процессе тестирования мы соберем некоторую статистику по необходимому размеру дискового пространства. Стоит задача организовать некий циклический архив для пользователя.

Каким образом это проще всего сделать?

Собственно, сабж.

Книга «Рандомизация и бутстреп: статистический анализ в биологии и экологии с использованием R»:

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

Скачать бесплатно без смс

• 4 июня 1996 года европейская ракета-носитель Ariane 5 развалилась на части на 39 секунде полета из-за ошибки в ПО (64bit float -> 16bit int). ущерб — 7 млрд. вечнозеленых;
• февраль 1991 года, ракета Patriot промахнулась мимо цели из-за ошибки округления, успела пролететь 500 метров. ущерб — 28 убитыми, сотня ранеными;
• 1987 год, медицинский ускоритель Therac-25 переоблучал пациентов с онкологическими заболеваниями из-за race condition. ущерб — несколько смертей;
• 1991 год, нефтяная платформа Sleipner A затонула после землетрясения силой 3 балла из-за ошибки в программе моделирования. ущерб — 700 млн.

А какие есть еще истории глобальных факапов, произошедших из-за ошибки в программном обеспечении?

В компанию РОН-Телеком нужен Erlang-программист.

Некоторые формальные требования:

• опыт разработки под GNU/Linux;
• опыт программирования на Erlang или желание это опыт приобрести;
• уверенное владение языками C и/или C++;
• опыт работы с СУБД, понимание базовых принципов;
• знание классических алгоритмов и структур данных;
• понимание работы сетевых протоколов;
• умение тестировать свой код;
• опыт работы с системами контроля версий git, svn;
• английский язык на уровне чтения документации и общения с коллегами по электронной почте;
• готовность работать под NDA;
• bash/tcl/perl/python для автоматизации ручной работы.

Работать надо в офисе в центре Челябинска, удаленки нет, ДМС нет.

Зарплата обсуждается на собеседовании, нижняя планка 40 тыр.

Также готовы взять молодых специалистов без опыта и студентов старших курсов. Обучение за счет конторы. Зарплата от 20 тыр.

Контакты в профиле.

В результаты поисковой выдачи неплохо бы добавить раздел Job, дабы искать вакансии, соответствующие поисковому запросу.

Дискасс.

Есть заброшенный проект под лицензией BSD:

Copyright (C) 2009 Enrique Marcote, Miguel Rodriguez All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of ERLANG TRAINING AND CONSULTING nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

Мы внесли в него много изменений: понаписали тестов, прикрутили dialyzer, исправили ошибки и т.п. Теперь есть желание выложить все это дело в open source.

Вопрос специалистам по всему: как грамотно оформить форк? Нужно ли менять название проекта? Как правильно указывать новые копирайты?

Словом, ткните в нужные маны.

Бертран Мейер выступит 11 апреля 2013 г. в 11:00 в конферец-зале ИВМиМГ СО РАН (ВЦ) с лекцией «Достижения в области параллельного программирования»

В настоящее время профессор Мейер возглавляет Chair of Software Engineering в Цюрихе, является CTO компании Eiffel Software, а также возглавляет кафедру программной инженерии и верификации программ в ИТМО.

http://www.iis.nsk.su/ershov_lectures/2013

копипаста с опеннета

Компании Red Hat и Rackspace добились решения федерального суда США о досрочном отклонении претензий по всем пунктам в патентном иске, предъявленном компанией Uniloc. Компания Uniloc, в 1990-х годах активно продававшая свои собственные разработки, в настоящее время является известным патентным троллем с обширной историей исков, в том числе против таких хай-тек компаний как Adobe, Microsoft, Sony и Symantec. Изначально иск был подан против компании Rackspace, использующей на своих серверах дистрибутив RHEL, в котором по заявлению Uniloc был зафиксирован факт нарушения одного из патентов. Компания Red Hat в рамках программы Open Source Assurance предоставляет клиентам защиту от патентных исков, поэтому также подключилась к судебному разбирательству.

Так победим!

true_admin, ты больше не модератор?

Я опять что-то пропустил?

Факультет свободных искусств и наук СПбГУ 27 марта 18:00 — открытая лекция Роджера Пенроуза (Оксфордский университет) «Нужна ли новая физика, чтобы понять мозг? Почему я не верю, что можно создать мозг на основе существующих теорий искусственного интеллекта» («Is New Physics Needed to Understand the Mind? Why I do not believe a Mind will be built on the basis of current theories of Artificial Intelligence.»)

Язык лекции: английский

Адрес: СПбГУ, Факультет свободных искусств и наук, Дворец Бобринских, ул. Галерная 58-60, Кинозал (ауд. 223)

http://artesliberales.spbu.ru/events/2013

Дополнение

Просьба к гостям факультета иметь при себе паспорт (это требование охраны) и заранее отправить короткое сообщение на электронный адрес andrei@philomatica.org указав в качестве темы сообщения «лекция Пенроуза». Дополнительную информацию можно получить у Андрея Родина andrei@philomatica.org

http://club.pdmi.ras.ru/moodle/

Как известно, lorcode осиливает небольшая часть рекрутеров и прочих работодателей. Поэтому мы и наблюдаем в разделе Job over 9000 тем с вырвиглазным и нечитаемым форматированием.

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

Дискасс.

Уникальный «воздушный дисплей» DisplAir, созданный астраханскими разработчиками, поступит в продажу 28 марта и будет стоить 398 000 рублей.

бла-бла-бла

DisplAir проецирует изображение на турбулентный поток твердых частиц воды размером до 2 мкм, свойства которых позволяют фиксировать до 1500 одновременных касаний. Эти твердые микрочастицы устойчивы к жаре и морозу: они не испаряются и не замерзают.

http://hi-tech.mail.ru/news/misc/air_display.html

А теперь вопрос: чего они натолкали внутрь за 400 тыр?