Спасибо за информацию — я обязательно посмотрю OberonScript как возможный инструмент для онлайнового обучения, альтернативный таким сайтам с JavaScript и Python. Сейчас вспоминаю, приятель использовал для школьного программистского кружка Pascal-среду, спрошу у него, был это BlackBox или что-то другое.
Здравствуйте, я с Обероном знаком поверхностно (читал первое описание языка — кажется, в конце 80-х, немного следил за новостями, которые довольно редки), но в университетские годы реализовывал в студенческом коллективе Модулу-2 и немного писал прикладной софт на ней. Я предварил данный комментарий этим вступлением в попытке вас заинтересовать до степени получения ответного комментария — убедить в серьёзности моих двух вопросов:
№1: Существуют ли (и, если не существуют, планируются ли кем-либо) для Оберона средства автоматизированного доказательства правильности кода? (для примера — вот недавняя история про планомерное применение такого средства к стандартным функциями Java: habrahabr.ru/post/251751)
№2: Рассматривает ли кто-либо в Оберон-сообществе идею создания «богатой» педагогической направленности системы с Обероном в качестве языка, на котором пишут код ученики? Я недавно поверхностно исследовал тему и обнаружил, что из «взрослых» ЯП (т.е. вычёркивая Scratch и подобные системы «только для детей») наиболее богато в этой роли используются JavaScript (на Khan Academy, прежде всего) и Пайтон (что, на мой взгляд, не так уж сильно отличается от JavaScript). Пояснение насчёт эпитета «богатой» — легкодоступной для детей / непрофессионалов и естественно поддерживающей социализацию учебного / творческого процесса, как и продуктивную самостоятельную работу учеников без людей-менторов / с минимальным вложением сил менторов (эти аспекты обеспечивают успех и ценность сайтов калибра Khan Academy).
Если вы думаете над унификацией по проектам с коллективной разработкой, имеет смысл рассмотреть устоявшийся хорошо документированный фреймворк — про один из таких есть, на мой взгляд, толковая книга автора по имени Miro Samek «Practical UML Statecharts in C/C++, Second Editiion. Event-Driven Programming for Embedded Systems». Собственно, очевидное преимущество описываемого там фреймворка (автор назвал его QP, Quantum leaPs) — сам факт существования книги :) (я первое издание читал в бумажной копии, теперь имею pdf второго издания, прочту, когда реально понадобится).
(заглянул на сайт автора — у него, оказывается, графический инструмент ещё появился для моделирования, ещё один плюс...)
Извините, жду TypeScript 1.0, и его в этом обновлении таки-прибудет:
•Deliver TypeScript 1.0 RC for Visual Studio 2013.
TypeScript is an open-source language that makes it easier to create cross-platform, large-scale JavaScript applications that run on any browser or host. TypeScript offers developers the advantages of strongly-typed languages on top of the flexible, dynamic runtime, and the ubiquity of JavaScript. TypeScript, a typed superset of JavaScript that compiles to plain JavaScript, works seamlessly with existing JavaScript tools and libraries, and easily integrates with existing applications and sites. TypeScript's native types and class-based modular programming model enable scalability and better productivity through early error detection and enhanced tooling, such as Intellisense, code refactoring, and code navigation. For more information about TypeScript, go to the TypeScript website
Интересно. Вы профи в теме (глядя на ваши реплики выше), а я знаком с ней только из любопытства, прочитал несколько статей / презентаций на английском, так что я не чувствую себя достаточно квалифицированным для обсуждения в подробностях. Основной пункт для меня вот в чём: насколько я могу понять беглым поиском, сублинейные алгоритмы с предподготовкой (Contraction Hierarchies) на Хабре не описывались. Да, они имеют недостатки при добавлении специфических (жизненных, разумеется) усложнений вроде динамики весов, ограничений, и не дают выигрыша на произвольных графах. Однако, они весьма хорошо работают на статических материковых картах (так как естественно сложившиеся материковые карты имеют достаточно низкую хайвейную размерность). Да, при добавлении динамики / ограничений в алгоритмы доказанной оптимальностью маршрутов приходится жертвовать, но то, что они резко проиграют после этого A*, это вопрос для меня не очевидный. Про динамику я статьи не читал, но они существуют (я интересовался, чем занимались авторы прочитанных мной статей в последнее время, и видел публикации про динамически усложнения).
Вот, кстати, пример статьи на Хабре: habrahabr.ru/post/180269/ — оригинальное исследование, весьма вероятно на идеях близких к Contraction Hierarchies (вершины графа с большими степенями лежат на хайвейных шорткатах в другой терминологии), но без отсылок к смежным исследованиям (довольно многочисленным и разнообразным: область ведь довольно горячая); меня это несколько опечаливает. А сесть самому в выходные, написать код, погонять, написать обстоятельное изложение и т.п. при том, что это никак не относится к моей текущей работе, я не могу себе позволить, увы (ну и не особо осмысленно «соревноваться» с профессионалами в области или работать популяризатором их результатов на чистом энтузиазме). А вы не собираетесь написать свою заметку? Интересно было бы почитать-обсудить!
Да-да, почему только Дейкстра и A*, когда из-за возросших в последние десятилетия потребностей (дорожные карты материкового масштаба, на которых надо быстро находить оптимальный маршрут между любыми парами точек; линейные по сложности алгоритмы становятся неприемлемыми) сейчас существуют хорошо проработаные алгоритмы, дающие сублинейную сложность поиска кратчайшего пути (если граф дорог удовлетворяет определённым критериям и есть возможность провести его пред-обработку). Это интересная тема, и я не видел пока на Хабре её обсуждений, хотя посты по поиску кратчайшего пути время от времени появляются! Но в них всегда те же Дейкстра и A*, плюс, может быть, эвристические улучшения… Поправьте меня, если здесь всё-таки описывали что-то более актуальное (ключевые словосочетания, например, contraction hierarchies, highway dimension — при удовлетворении пред-условий на дорожную сеть сублинейный результат по сложности гарантируется, никаких эвристических неопределённостей!)
Я не имею в виду, что в этой заметке неправилный подход (тут акцент на других аспектах), просто пока не вижу на Хабре добротной информации по современным алгоритмам поиска кратчайшего пути на дорожных сетях за сублинейное время.
Да, сейчас поискал ещё раз, есть только одно упоминание highway dimension — но не в заметке, а в объявлении о лекции: habrahabr.ru/company/yandex/blog/82992/
Солидаризуюсь — я имел дело с C++ проектами, в которых использовался Doxygen, это было удобно (разметка комментариев легковесная, производная от Javadoc — в сравнении с, например более тяжёлой XML разметкой Sandcastle — и сгенерированная документация выглядит пристойно).
О, я тоже на этот топик только сейчас наткнулся — искал, что пишут на Хабре про Coq… Так вот, у автора этой записи ymn есть небольшой вводный тьюториал по Coq из нескольких записей. В конце первой есть ссылки на 2 книги: «Software Foundations» и «Certified Programming with Dependent Types» — я думаю, это и есть вышеупомянутые «два отличных учебника».
По-моему, этот минус (если он так уж беспокоит) преодолим посредством «выворачивания» дерева в месте последней модификации на манер finger tree. Я подумывал скомбинировать органицацию набора блоков приличной длины (а не по несколько символов, как если бы finger tree использовалось в лоб для хранения массива символов) с выворачиванием, а ещё рассматривал забавную идею immutable блока с гэп-буфером: давайте контрольную запись (указатель на блок плюс индексы краёв гэпа) хранить отдельно от самого блока. Тогда при добавлении символов на краях гэпа блок клонировать не надо — создаются новые контрольные записи с обновленными индексами краёв гэпа (гэп сужается) — старые контрольные записи продолжают оставаться в том же состоянии (immutable), указывая на тот же блок!
Товарищи на видео (и конкретно Хейслберг) обсуждают эту область как вторую по популярности просьбу (первая — generics — выполнена). В версии 1 этой фичи точно не будет — причина в недостаточной определённости текущего драфта ECMAScript 6 в смежной области, насколько я понял: без продвижения этого драфта сгенерированный из конструкций async / await JS код будет сильно отличаться от оригинального TS, а это входит в противоречия с намереньями авторов TS.
В идеале особой разницы быть не должно (более того, в некоторых подразделениях её устраняют формально), но на практике «менталитет», так сказать, отличается (ну и критерии отбора кандидатов при найме другие). Пост этого сотрудника (Ahmet Alp Balkan) мне напомнил личных знакомых-программистов, которые, будучи несчастливо нанятые в тестовые подразделения, воспряли, переведясь в разработчики. Впрочем, один мой знакомый, очень продуктивный программист-энтузиаст, прекрасно чувствует себя и в тестовом подразделении (возможно, повезло с командой / начальником… Исключение, подтверждающее правило?)
Насколько я понимаю, в подразделении, в котором трудится автор исходного поста (Ahmet Alp Balkan) пишут по большой части на C# (тем более, он в тесте, не в девелопменте). По части C++11 — ситуация неоднозначная, на мой взгляд. Давайте взглянем на что-то довольно новое — разработку на С++ под плиточный интерфейс Windows 8 (ранее называвшийся «Метро»).С одной стороны, языковые нововведения C++11 задействованы, и их использование приветствуется (характерный, бросающийся в глаза пример — лямбда-выражения для программирования асинхронных операций). С другой — в этом контексте предлагается программировать на так называемом C++/CX, как наиболее удобном варианте программирования «на C++» в этом контексте — и это действительно так!.. Но этот нестандартное расширение C++. Можно следовать такой тактике: писать код на стандартном C++11, изолируя системно-зависимую логику в хорошо ограниченной группе C++/CX исходников.
Забавно — парня, написавшего исходный пост наняли в тестовую организацию Azure (это явно высказано в диалоге с Хансельманом в комментариях), а он со своей колокольни эдак обобщительно и за девелоперов пишет — ну, ветер ему в паруса.
Да, согласен, задача несколько другая, но смежная — я всё-таки подумываю о пересказе того, что просматривал на досуге; темы переплетаются (и, как показывает беглый поиск, здесь на Хабре заинтересовавшие меня вопросы пока не обсуждались). Один из интересных пунктов — формальное определение оного свойства «фрактальности», при соблюдении которого для большой карты увеличение размера памяти для хранения МКР-информации всей карты — фиксированный множитель. Не буду вдаваться в детали, потому что могу легко что-нибудь напутать из памяти — надо сесть, вдумчиво пересмотреть статьи / презентации. Если таки-доведу идею написать запись по теме до успешного воплощения, помещу здесь ссылку.
А вы не рассматривали алгоритмы с многоуровневыми вспомогательными графами на подобие МКР? Если вам это любопытно, могу найти ссылки на статьи и, возможно, слайды (на английском, правда). Интересная деталь, которая мне вспоминается про эту область (я по работе с ней дела не имею, ознакомился поверхностно на досуге) — определённое свойство «фрактальности» графа дорожной сети там определяется формально, и для типичных графов континентального масштаба оно действительно выполняется (в одной из статей есть даже рассуждения на тему, что так получается из-за исторически инкрементального развития сети дорог). Оно, правда, не выполняется, например, на регулярных сетках типа расчерченного строго перпендикулярными улицами района города.
Практический аспект — континентальные дорожные сети очень велики и алгоритмы линейной сложности по размеру графа не удовлетворяют практическим требованиям, нужны алгоритмы суб-линейные по сложности (которые как раз существуют для пред-обработанных графов с пред-вычисленной дополнительной информацией, аналогичной многоуровневым МКР). О, кстати, бегло пробежавшись по ссылкам, увидел знакомую фамилию по последней ссылке — Голдберг, я был как раз на его презентации однажды (на которой он излагал теорию и практику этого подхода).
Тут имеется некоторый исторический аспект. Из эвклидовой геометрии тоже выросло дерево, не настолько пышное, но более вписавшееся в современный контекст (да, есть неэвклидова геометрия, но она не отменяет логические построения эвклидовой геометрии — просто имеет другую аксиоматику).
Аристотелева логика же, трудами раннехристианских философов и, позднее, средневековых схоластов была возведена в ранг догмы, что выхолостило её рациональное зерно (при полном отказе от критики) и затормозило развитие формальной логики как научной дисциплины на столетия, если не на тысячелетие.
Бертран Рассел (мне недавно попался соответствующий фрагмент в его «Истории западной философии») указывает на определённые слабости Аристотелевой логики, вот ссылка на цитату (по-английски, можно при желании найти русский перевод): www.physicsforums.com/showthread.php?t=537913.
Применительно к фразе «все кентавры говорящие» его рассуждения звучат примерно так. Рассматривая похожие и неразличаемые в Аристотелевой логике фразы «Фол — говорящий» (Фол — субъект, конкретный кентавр) и «все кентавры говорящие» Рассел указывает на то, что подразумеваемое прочтение второй фразы приводит к выводу, чту у неё субъекта (в понятном смысле, как в первой фразе) нет. Подразумеваемое прочтение второй фразы у него такое: она эквивалентна конъюнкции фраз «существуют кентавры» и «если что-то есть кентавр, это что-то — говорящее» — ни в одной из них о «всех кентаврах» речи не идёт.
(думаю заглянуть-таки в русский перевод за цитатами и запостить здесь более дельное резюме его критики, показавшейся мне довольно обоснованной)
Классно, удачи с помидорами — я на всякий случай снова нашёл и сохранил чужое аналитическое решение (отличное от моего, «физического», тем, что для доказательства правильности аналитического решения ничего особо не надо, в то время как в «физическом» у меня дыры из-за пробелов в образовании — я программист, а не математик, хотя и учился на мат-мехе). Я в этом чужом решении так досконально и не разобрался (оно записано очень сжато, а интерес к задаче я уже потерял).
Да, вы правы; однако, усложнять формулировку в надежде, что она останется достаточно изящной, мне лень. Кстати у меня есть про запас совсем другая задача, в которой в пределе получается такая вероятность (1 — 1/e), без ошибок — «задача про гниющие помидоры» (автор задачи — Ольга Леонтьева). Надо бы напрячься и опубликовать здесь отдельной записью. Мне удалось решить её только «физическим» способом, хотя она комбинаторная (через переход к непрерывной функции, предполагая, что её непрерывность и дифференцируемость доказывается — и затем решая дифур), но у неё есть и честное комбинаторное решение (которое мне найти было слабо, но добрые люди помогли… надеюсь, у меня его запись где-то сохранилась).
№1: Существуют ли (и, если не существуют, планируются ли кем-либо) для Оберона средства автоматизированного доказательства правильности кода? (для примера — вот недавняя история про планомерное применение такого средства к стандартным функциями Java: habrahabr.ru/post/251751)
№2: Рассматривает ли кто-либо в Оберон-сообществе идею создания «богатой» педагогической направленности системы с Обероном в качестве языка, на котором пишут код ученики? Я недавно поверхностно исследовал тему и обнаружил, что из «взрослых» ЯП (т.е. вычёркивая Scratch и подобные системы «только для детей») наиболее богато в этой роли используются JavaScript (на Khan Academy, прежде всего) и Пайтон (что, на мой взгляд, не так уж сильно отличается от JavaScript). Пояснение насчёт эпитета «богатой» — легкодоступной для детей / непрофессионалов и естественно поддерживающей социализацию учебного / творческого процесса, как и продуктивную самостоятельную работу учеников без людей-менторов / с минимальным вложением сил менторов (эти аспекты обеспечивают успех и ценность сайтов калибра Khan Academy).
(заглянул на сайт автора — у него, оказывается, графический инструмент ещё появился для моделирования, ещё один плюс...)
•Deliver TypeScript 1.0 RC for Visual Studio 2013.
TypeScript is an open-source language that makes it easier to create cross-platform, large-scale JavaScript applications that run on any browser or host. TypeScript offers developers the advantages of strongly-typed languages on top of the flexible, dynamic runtime, and the ubiquity of JavaScript. TypeScript, a typed superset of JavaScript that compiles to plain JavaScript, works seamlessly with existing JavaScript tools and libraries, and easily integrates with existing applications and sites. TypeScript's native types and class-based modular programming model enable scalability and better productivity through early error detection and enhanced tooling, such as Intellisense, code refactoring, and code navigation. For more information about TypeScript, go to the TypeScript website
.
Вот, кстати, пример статьи на Хабре: habrahabr.ru/post/180269/ — оригинальное исследование, весьма вероятно на идеях близких к Contraction Hierarchies (вершины графа с большими степенями лежат на хайвейных шорткатах в другой терминологии), но без отсылок к смежным исследованиям (довольно многочисленным и разнообразным: область ведь довольно горячая); меня это несколько опечаливает. А сесть самому в выходные, написать код, погонять, написать обстоятельное изложение и т.п. при том, что это никак не относится к моей текущей работе, я не могу себе позволить, увы (ну и не особо осмысленно «соревноваться» с профессионалами в области или работать популяризатором их результатов на чистом энтузиазме). А вы не собираетесь написать свою заметку? Интересно было бы почитать-обсудить!
Я не имею в виду, что в этой заметке неправилный подход (тут акцент на других аспектах), просто пока не вижу на Хабре добротной информации по современным алгоритмам поиска кратчайшего пути на дорожных сетях за сублинейное время.
Да, сейчас поискал ещё раз, есть только одно упоминание highway dimension — но не в заметке, а в объявлении о лекции: habrahabr.ru/company/yandex/blog/82992/
Практический аспект — континентальные дорожные сети очень велики и алгоритмы линейной сложности по размеру графа не удовлетворяют практическим требованиям, нужны алгоритмы суб-линейные по сложности (которые как раз существуют для пред-обработанных графов с пред-вычисленной дополнительной информацией, аналогичной многоуровневым МКР). О, кстати, бегло пробежавшись по ссылкам, увидел знакомую фамилию по последней ссылке — Голдберг, я был как раз на его презентации однажды (на которой он излагал теорию и практику этого подхода).
Аристотелева логика же, трудами раннехристианских философов и, позднее, средневековых схоластов была возведена в ранг догмы, что выхолостило её рациональное зерно (при полном отказе от критики) и затормозило развитие формальной логики как научной дисциплины на столетия, если не на тысячелетие.
Применительно к фразе «все кентавры говорящие» его рассуждения звучат примерно так. Рассматривая похожие и неразличаемые в Аристотелевой логике фразы «Фол — говорящий» (Фол — субъект, конкретный кентавр) и «все кентавры говорящие» Рассел указывает на то, что подразумеваемое прочтение второй фразы приводит к выводу, чту у неё субъекта (в понятном смысле, как в первой фразе) нет. Подразумеваемое прочтение второй фразы у него такое: она эквивалентна конъюнкции фраз «существуют кентавры» и «если что-то есть кентавр, это что-то — говорящее» — ни в одной из них о «всех кентаврах» речи не идёт.
(думаю заглянуть-таки в русский перевод за цитатами и запостить здесь более дельное резюме его критики, показавшейся мне довольно обоснованной)