← All posts tagged Spark

OCTAGRAM
ada GNAT У AdaCore обновилась страница загрузки GNAT
На один дебилизм стало меньше. Раньше у них выбор начинался с года, а потом шли платформы. Если в каком-то году нет платормы, то её даже в списке не было. Потом сделали, чтоб было, но серого цвета. Это касается всяких экспериментальных платформ типа LEGO NXT MindStorm, на смену которому пришёл ARM для голых досок. А также JVM и CLI, которые кроме гуглострадальцев (AppEngine) оказались почти никому не нужны, когда есть нормальные (нативные) компиляторы. Если всё же хочешь скачать, перебирай разные года, пока не найдёшь нужный. Сейчас, если зайти в more platforms, все платформы в списке можно выбрать, и сам выбирается наибольший год выпуска.

Я бы ещё SPARK до 2012го года включительно отдельно выделял, потому что в старом СПАРКе аннотации для верификатора в комментариях специального вида пишутся, и это совместимо с, например, MapuSoft AdaMagic, BTC ObjectAda, BTC Apex Ada, Janus Ada, Irvine и пр. застрявшими между Ada 95 и Ada 2005, а аннотации SPARK 2014 пишутся в аспектах, которые поддерживает только GNAT. Понятно, что AdaCore не сильно заинтересованы в поддержке конкурентов.

Ещё заметил, что на страницу загрузки теперь можно попасть, не оставляя свой email.

Теперь, наверное, самым ожидаемым был бы кроссплатформенный пакетный менеджер с онлайн базой данных. Это было бы логичным продолжением линии развития gnatmake => gprmake => gprbuild+gprinstall. Даже в Делфи свой уже появился.
OCTAGRAM
конкурс ARM embedded Spark ada Началось соревнование «Make with Ada» для разработчиков встраиваемых систем
AdaCore организует новый конкурс для разработчиков. Как и в прошлые разы, на подготовку даётся существенно больше времени, чем в олимпиадах по иноформатике. Это как раз подходит тем, кому не нравятся соревнования по быстрому написанию страшного кода, который потом только выбросить.

Сегодня на повестке дня — разработка для ARM на голом железе и технологии верификации. Общий призовой фонд — более 8000€.

makewithada.org

Как бы отвечая на напрашивающийся вопрос, — да, я уже посмотрел на логотип через анаглиф очки.
OCTAGRAM
DNS Spark ada ironsides.martincarlisle.com
Адский DNS сервер

IRONSIDES is an authoritative/recursive DNS server pair that is provably invulnerable to many of the problems that plague other servers. It achieves this property through the use of formal methods in its design, in particular the language Ada and the SPARK formal methods tool set. Code validated in this way is provably exception-free, contains no data flow errors, and terminates only in the ways that its programmers explicitly say that it can. These are very desirable properties from a computer security perspective.
OCTAGRAM
Erlang pascal ada silver Разработчики Silver, в отличие от разработчиков Free Pascal, черпают вдохновение не из C++, а из более подходящей Ada, и тем самым автоматически получают уважение:
But with Elements 8.0, RemObjects are going further and introducing Not Nullable references types. That is, the declaration of a variable dictates that it must hold a reference and cannot be null.deltics.co.nz

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

Тем временем в AdaCore экспериментируют с легковесной многопоточностью, делают язык программирования, стоящий в одном ряду с Erlang, Limbo, Rust, Go. Ada была выбрана из четырёх вариантов языка, имевших кодовые имена, цветов. Если я всё правильно помню, в Ada 83 победил Green, а к разработке Ada 95 подключились люди, делавшие Red. Чем–то в ускоренном варианте напоминает эту изторию разработка адского клона эрланга. В лабораториях AdaCore придумали экспериментальные Sparkel, Parython и Javallel, по синтаксису берущие начало от SPARK (подмножество Ada), Python и Java, соответственно, а потом взяли из них всё лучшее и получился ParaSail. Отличие от Erlang, Go и других языков в том, что в них зелёная многопоточность явная, нужно делать spawn, а в ParaSail и товарищах (в текущей версии они все компилируются в один байт–код и могут выполняться на одной и той же виртуальной машине) — в самом синтаксисе языка есть конструкции, допускающие разбиение на зелёные подзадачи. А компилятор убедится в безопасности доступа к данным.
parasail-programming-language.blogspot.ru

Для production ParaSail и товарищи пока сырые. В частности, работать с HTTP и XML я на них пока не смог. А жаль. Не выгорело с Erlang, хоть на Sparkel перевёз бы node.js проекты.