Результаты поиска по запросу «[ocaml]»

Objective CAML

SHK — Fri, 06 Nov 2009 13:48:32 GMT

Objective CAML — один из гибридных языков программирования, то есть поддерживающий несколько парадигм программирования, в данном случае у нас это объектно-ориентированное программирование и функциональное программирование. Как известно, сильными сторонами функционального программирования являются: надежность кода, удобство тестирования, возможность оптимизации при компиляции и т.д. Но несмотря на все достоинства функционального программирования, так же присутствуют и минусы, такие как: отличающийся стиль написания программ от императивного, зачастую нехватка хорошей литературы, неудобный синтаксис и т.д.
Если кого — либо заинтересует, рискну рассказать по подробнее об этом языке программирования.

Ocaml Tools

SHK — Fri, 06 Nov 2009 14:59:52 GMT

Сегодня я постараюсь рассказать вам об инструментах, помогающих программировать на Objective CAML.
Продолжение

Списки и другие структуры данных в Ocaml

SHK — Mon, 09 Nov 2009 06:08:51 GMT

Введение

Кроме базовых типов данных в Objective Caml к предопределенным типам относятся кортеж, список, запись.
Продолжение

PG'OCAML = PostgreSQL + OCaml

SHK — Wed, 18 Nov 2009 08:29:38 GMT

Cегодня понадобилось обратиться к базе данных PostgreSQL из Objective Caml, наиболее удобным и продвинутым фремворком для работы с PostgreSQL оказался — PG'OCAML. В этом посте хотелось бы показать пару примеров связки Objective Caml и PostgreSQL и насколько это просто.
Продолжение

Взлом TLS с денежным призом

alizar — Wed, 11 Feb 2015 13:30:46 GMT

Разработчики TLS-имплементации на языке OCaml объявили конкурс BTC Piñata, чтобы доказать надёжность своей защиты. Известно, что конкурсы не могут быть настоящим доказательством, но этот очень уж забавный, да ещё с небольшим денежным призом.

Итак, двое хакеров открыли демо-сервер ownme.ipredator.se.

На сервере лежит ключ от биткоин-адреса 183XuXTTgnfYfKcHbJ4sZeF46a49Fnihdh. Сервер отдаст нам ключ, если мы предъявим сертификат.

Организаторы предусмотрели механизм MiTM для нас. Мы можем пропускать через себя трафик между виртуальными машинами BTC Piñata (TLS-сервер и TLS-клиент). Как понятно, в этом трафике есть нужный сертификат, нужно его только извлечь каким-то образом.
Читать дальше →

[Перевод] Как я нашёл баг в процессорах Intel Skylake

m1rko — Thu, 06 Jul 2017 12:24:53 GMT

Инструкторы курсов «Введение в программирование» знают, что студенты находят любые причины для ошибок своих программ. Процедура сортировки отбраковала половину данных? «Это может быть вирус в Windows!» Двоичный поиск ни разу не сработал? «Компилятор Java сегодня странно себя ведёт!» Опытные программисты очень хорошо знают, что баг обычно в их собственном коде, иногда в сторонних библиотеках, очень редко в системных библиотеках, крайне редко в компиляторе и никогда — в процессоре. Я тоже так думал до недавнего времени. Пока не столкнулся с багом в процессорах Intel Skylake, когда занимался отладкой таинственных сбоев OCaml.

Первое проявление

В конце апреля 2016 года вскоре после выпуска OCaml 4.03.0 один Очень Серьёзный Индустриальный Пользователь OCaml (ОСИП) обратился ко мне в частном порядке с плохими новостями: одно из наших приложений, написанное на OCaml и скомпилированное в OCaml 4.03.0, падало случайным образом. Не при каждом запуске, но иногда вылетал segfault, в разных местах кода. Более того, сбои наблюдались только на их самых новых компьютерах, которые работали на процессорах Intel Skylake (Skylake — это кодовое название последнего на тот момент поколения процессоров Intel. Сейчас последним поколением является Kaby Lake).

За последние 25 лет мне сообщали о многих багах OCaml, но это сообщение вызывало особенное беспокойство. Почему только процессоры Skylake? В конце концов, я даже не мог воспроизвести сбои в бинарниках ОСИПа на компьютерах в моей компании Inria, потому что все они работали на более старых процессорах Intel. Почему сбои не воспроизводятся? Однопоточное приложение ОСИПа делает сетевые и дисковые операции I/O, так что его выполнение должно быть строго детерминировано, и любой баг, который вызвал segfault, должен проявлять себя при каждом запуске в том же месте кода.
Читать дальше →

[Перевод] Сравнение одинакового проекта в Rust, Haskell, C++, Python, Scala и OCaml

m1rko — Tue, 18 Jun 2019 16:32:26 GMT

В последнем семестре университета я выбрал курс компиляторов CS444. Там каждая группа из 1-3 человек должна была написать компилятор из существенного подмножества Java в x86. Язык на выбор группы. Это была редкая возможность сравнить реализации больших программ одинаковой функциональности, написанных очень компетентными программистами на разных языках, и сравнить разницу в дизайне и выборе языка. Такое сравнение породило массу интересных мыслей. Редко можно встретить такое контролируемое сравнение языков. Оно не идеально, но намного лучше, чем большинство субъективных историй, на которых основано мнение людей о языках программирования.

Мы сделали наш компилятор на Rust, и сначала я сравнил его с проектом команды на Haskell. Я ожидал, что их программа будет намного короче, но она оказалась того же размера или больше. То же самое для OCaml. Затем сравнил с компилятором на C++, и там вполне ожидаемо компилятор был примерно на 30% больше, в основном, из-за заголовков, отсутствия типов sum и сопоставлений с образцом. Следующее сравнение было с моей подругой, которая сделала компилятор самостоятельно на Python и использовала менее половины кода, по сравнению с нами, из-за мощности метапрограммирования и динамических типов. У другого товарища программа на Scala тоже была меньше нашей. Больше всего меня удивило сравнение с другой командой, которая тоже использовала Rust, но у них оказалось в три раза больше кода из-за разных дизайнерских решений. В конце концов, самая большая разница в количестве кода оказалась в пределах одного языка!
Читать дальше →

Формальная верификация кода на Coq: тактики

Natasha_Klaus — Tue, 18 Jul 2023 10:00:45 GMT

Данная статья является адаптированным переводом моей статьи: Formalization of code in Coq - tactics, написанной в период работы над проектом coq-tezos-of-ocaml.

Суть проекта: часть исходного кода протокола криптовалюты Tezos была переведена на Coq, а затем верифицирована с помощью математических методов и формальной логики.

Статья предназначена для круга читателей, имеющих опыт работы с Coq.

Часто процесс формальной верификации становится утомительным и монотонным из за повторяющихся действий, которые пруф-инженеру (от английского слова proof - доказательство) приходится выполнять. К счастью, в Coq есть инструменты и техники автоматизации доказательств, которые позволяют не только значительно увеличить производительность, но и сделать доказательства короче.

В данной статье мы покажем, как использовать и писать тактики на примере формальной верификации исходного кода криптовалюты Tezos (написанной на OCaml), а именно, мы затронем следующие темы:

Ocaml. Типы данных

SHK — Sat, 07 Nov 2009 14:36:37 GMT

Введение

В этом посте перейдем непосредственно к ознакомлению с языком Objective Caml. В этом посте будет рассказано об базовых типах данных Objective Caml.
Для начала вам необходимо скачать и установить Objective Caml, на этом этапе достаточно будет одного интерпретатора. Запуск интерпретатора производится с помощью: команды ocaml, если дело происходит в *nix, либо запуска ocaml.exe если дело происходит в Windows.
После запуска интерпретатора мы увидим следующее: версию Ocaml, у меня это Objective Caml version 3.00, и ожидание ввода команд:#.
Каждая логическая единица кода — фраза, заканчивается в Objective Caml — ;; Выход из интерпретатора, осуществляется либо по нажатию Сtrl+D, либо после вызова функции exit типа int -> int:
exit 0;;
Продолжение

Цепной квайн

icCE — Tue, 10 Nov 2009 12:39:24 GMT

Один японец написал забавный цепной квай.
Что такое квайн?.

посмотреть,что он написал

[Перевод] Введение в OCaml: The Basics [1]

amarao — Sun, 21 Nov 2010 03:29:05 GMT

(предисловие от переводчика: сел учить окамл, обнаружил, что отсутствует перевод на русский язык руководства для начинающих. Восполняю этот пробел).

Основы

Другими словами, комментарии в OCaml очень похожи на комментарии в Си (/* ... */).

В настоящий момент нет однострочных комментариев (как #... в Перле или // ... в C99/C++/Java). Когда-то обсуждалась возможность использовать ## ..., и я весьма рекомендую окамловским товарищам в будущем добавить эту возможность (однако, хорошие редакторы открывают возможность использования однострочных комментариев даже сейчас).

Комментарии в OCaml вложенные, это позволяет очень просто комментировать куски кода с комментариями:

(* This code is broken ...



(* Primality test. *)

let is_prime n =

(* note to self: ask about this on the mailing lists *) XXX;;



*)

Вызов функций

Допустим, вы написали функцию, назовём её repeated, которая берёт исходную строку s, число n и возвращает новую строку, состоящую из n раз повторённой строки s.

В большинстве С-подобных языков вызов функции будет выглядеть так:
repeated ("hello", 3) /* this is C code */

Это означает «вызвать функцию repeated с двумя аргументами, первый аргумент — строка hello, второй аргумент — число 3».

Подобно остальным функциональным языкам программирования, в OCaml, запись вызовов функций и использование скобок существенно отличается, что приводит к множеству ошибок. Вот пример того же самого вызова, записанного на OCaml: repeated "hello" 3 (* this is OCaml code *).

Обратите внимание — нет скобок, нет запятых между аргументами.
Читать дальше →

[Перевод] Введение в OCaml: Структура программ на OCaml [2]

amarao — Fri, 26 Nov 2010 01:55:20 GMT

[прим. пер.: продолжение перевода, первая статья тут]

Структура программ на OCaml

Теперь мы потратим немного времени на высокоуровневый анализ некоторых настоящих программ на OCaml'е. Я хотел бы показать вам локальные и глобальные определения, разницу в использовании ;; и ;, модули, вложенные функции, ссылки. Из-за этого мы столкнёмся с множеством концепций OCaml'а, которые пока что не имеют смысла для начинающего изучать OCaml, так как мы не встречали их ранее. Не фокусируйтесь на них, сконцентрируйтесь вместо этого на общем представлении о формате программ и особенностях языка, на которые я буду указывать.

Локальные «переменные» (на самом деле локальные выражения)

Возьмём нашу функцию average на Си и добавим в неё локальные переменные (сравните её с примером в прошлой главе).

double average (double a, double b)
{
  double sum = a + b;
  return sum / 2;
}

Теперь посмотрим на это для OCaml:

let average a b =
  let sum = a +. b in
  sum /. 2.0;;

Стандартное выражение let name = expression in используется для определения локального именованного выражения и name может быть использовано в дальнейшем вместо expression вплоть до ;;, который означает окончание локального блока кода. Обратите внимание, мы даже не использовали отступ после объявления in. Просто воспринимайте let ... in так, как будто это один оператор.
Читать дальше →

[Перевод] Введение в OCaml: Типы данных и сопоставление [3]

amarao — Sat, 04 Dec 2010 23:21:38 GMT

[прим. пер.: продолжение перевода. первая часть, вторая часть]

Связные списки

В OCaml, так же как в Perl, есть встроенная на уровне языка поддержка списков. Все элементы списка должны быть одного типа. Для определения типа используется выражение:

[1; 2; 3]

Обратите внимание: точка с запятой, а не запятая.

[] означает пустой список.

У списка есть голова (первый элемент) и хвост (остальные элементы, кроме головы). Голова — элемент. Хвост — список. В вышеприведённом примере голова — целое число 1, а хвост — список [2; 3].

Альтернативной формой записи является использование оператора конструирования (cons) в форме head :: tail. Нижеприведённые строки полностью эквивалентны друг другу.

[1; 2; 3]
1 :: [2; 3]
1 :: 2 :: [3]
1 :: 2 :: 3 :: []

Зачем мы упомянули оператор конструирования? Он полезен когда мы начинаем сопоставление с образцом для списков, мы обсудим это чуть позже.

Тип данных для связного списка

Тип данных для связного списка целых будет int list; общий тип для связного списка объектов типа foo будет foo list.
Читать дальше →

OCaml и PHP — эзотерика для вашего удобства

torkve — Tue, 13 Jul 2010 16:37:31 GMT

NB: читая этот топик, желательно не есть — можно поперхнуться от неожиданности.
NB: менее ценные куски кода пришлось вынести на пастебин, из-за того что хабр обрезает пост. Следите за ссылками в тексте.

Многие причисляют OCaml к маргинальным и даже эзотерическим языкам. Возможно они и правы, хотя множество людей с ними не согласны. Для меня знакомство с ним началось с полгода назад, когда мне в очередной раз захотелось научиться чему-то новому и я подумал, что хоть один функциональный язык надо освоить. Из множества языков я выбрал Objective Caml. Язык покорил меня человеческим синтаксисом и идеей: есть все функциональные радости жизни, но если хочешь императивный стиль и ООП — бери, их есть у меня! Оказалось, что разработчики прекрасно понимали, что для разных задач нужны разные средства. Три дня чтения мануала для C++ и Perl-программистов и я уже вполне мог читать код и писать хеллоуворлды. На этом моё знакомство с языком закончилось, потому что изучать язык не на реальной задаче — дело глупое.
А теперь о более реальной разработке

Ocsigen 2.0 — новая версия фреймворка для OCaml

torkve — Thu, 22 Sep 2011 10:50:11 GMT

Для тех, кто не знает: строго говоря, Ocsigen — это не совсем фреймворк. Ocsigen — это набор инструментов для создания эффективных веб-приложений на языке OCaml, он включает в себя как веб-сервер, так и инструменты для работы с потоками, написания расширений к веб-серверу, генерации HTML и многого другого. Кстати, замечу, что это может показаться невероятным (а кому-то может и не очень удобным), но генерируемый HTML5 или XHTML является статически типизированным, и валидность всего, что ваш сайт может сгенерить, будет проверена ещё на этапе компиляции.

Картинка для привлечения внимания — вращающаяся земля целиком написана на OCaml, а работает целиком в браузере.
Ну а вчера вышла новая версия этого замечательного фреймворка, и вот информация из анонса Винсента Балата (Vincent Balat): Прочитать о ней

Динамические приложения с Ocsigen или Йоба возвращается

torkve — Sun, 25 Sep 2011 11:07:09 GMT

Что делает холодным воскресным утром нормальный человек? Любой вам ответит: холодным воскресным утром человек спит. Потому что всю неделю он работал и хочет отдохнуть.
Что делает холодным воскресным утром программист? Холодным воскресным утром программист пьёт горячий чай и пишет код. Чай он пьёт, потому что утро холодное, да и проснулся ещё не до конца, а код пишет, потому что хочется. Программисту всегда хочется писать код, только в будни он пишет код за деньги и от этого очень устаёт, а в выходные для себя, поэтому отдыхает.

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

Как вы возможно помните, когда-то мы писали интерпретатор языка Йоба. С тех пор интерпретатор был незначительно улучшен, выделен в отдельный класс, стал принимать строку на вход, отдавать строку на выход (вместо работы с консолью). Теперь нашей задачей станет ~~внедрение Йобы в качестве основного языка компании Google~~ превращение интерпретатора Йобы в веб-приложение, да не простое — а клиентское. Хоть я и добавил в класс счётчик операций, чтобы нельзя было слишком обнаглеть, но всё равно — пусть пользователь на своём компьютере вычислительные мощности тратит, а не на сервере.
Поехали!

Melange — DSL для сетевых протоколов

torkve — Sat, 28 Dec 2013 20:07:01 GMT

Всем программистам рано или поздно приходится передавать данные. Ни для кого не секрет, что библиотек сериализации в Java существует примерно >9000, а в C++ они вроде и есть, а вроде их и нет. К счастью для большинства, несколько лет назад появился Google Protobuf, который принёс достаточно удобный способ определять структуры данных и быстро завоевал всенародную любовь. Это была фактически первая, доступная широким массам библиотека, позволяющая гонять по сети готовые структуры данных, не связываясь при этом с чем-то вроде XML. На дворе был 2008 год.

Вернёмся немного назад. В 2006 году простой индийский программист (как бы подозрительно это ни звучало!) Анил Мадхавапедди, один из самых известных сейчас в мире OCaml-разработчиков и автор свежевышедшей книги Real World OCaml, защищал в Кембридже кандидатскую диссертацию. Именно о ней я сегодня вам и расскажу.

Анил сразу пошёл дальше, чем Google. Он сразу подумал, для чего люди обычно пересылают по сети какие-то формализованные структуры данных? Чтобы реализовать какой-то протокол. А что такое протокол? Это какой-то конечный автомат. А где мы можем взять хороший пример сложного, хорошо спроектированного и проверенного временем протокола? Да прямо в обычном сетевом стеке! Итак, были взяты набор сетевых структур данных и протоколов: Ethernet frame, IPv4, ICMP, TCP, UDP, SSH, DNS и DHCP и постановка задачи: большая часть этих протоколов (особенно SSH и DNS) реализуются, что называется «руками», а хочется, чтобы не было типичных для C переполнений буфера, все переходы совершались автоматически, это всё можно было верифицировать, и чтобы работало быстро, а не как обычно.

Поскольку никто не будет читать диссертацию, сразу скажу: это более чем удалось. По результатам работы были написаны референсные реализации DNS и SSH-сервера и произведено сравнение с BIND и OpenSSH. OCaml-реализации давали по сравнению с традиционными прирост производительности от незначительного, до почти двухкратного. Кроме того была найдена ошибка в RFC на SSH (рабочая группа была уведомлена и RFC исправлен). О том, что было сделано, и как с этим жить, читайте под катом. Мне интересно.

Как сделать Laser Squad из XCOM: этюд для GDB в OSX

zbroyar — Wed, 15 Apr 2015 07:57:11 GMT

Вот так теперь выглядит игра Laser Squad, которую я увидел очень давно. Тогда она была во всех смыслах проще и выглядела так:

При этом принципиально игра не изменилась. Просто стала сложнее: куча типов ресурсов, множество вариантов их применения плюс «инфляция»: каждая следующая мастерская, лаборатория или спутниковый канал стоят больше, чем предыдущие. С одной стороны, это все дает возможность играть разными стратегиями развития, но иногда так хочется поиграть просто в Laser Squad! Поэтому…
Читать дальше →

[Перевод] Десять причин не использовать статически типизированный функциональный язык программирования

DarkCoder — Sun, 18 Aug 2013 19:13:31 GMT

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

Про автора

Я разработчик и архитектор британской не софтверной компании. Имею 20 летний опыт в различных областях от высоко-уровневых UX/HCI до низко-уровневых реализаций баз данных.
Несмотря на то что я использую C# в своей повседневной работе, я писал промышленный код на многих языках, мои любимые Smalltalk, Python и совсем недавно F# (поэтому я и создал этот сайт).

Разглагольствования по поводу того чего я не понимаю

Вам надоела вся эта шумиха вокруг функциональных языков? Мне тоже! Я выскажу по этому поводу несколько причин почему разумные люди, такие как мы с вами, должны держаться подальше от этого.

Немного поясню: когда я говорю «статически типизированный функциональный язык программирования», я подразумеваю языки, которые поддерживают вывод типов по-умолчанию и прочее. На практике это означает Haskell и семейство языков ML (включая OCaml и F#).
Читать дальше →

Скоро ICFPC 2016

unclechu — Tue, 02 Aug 2016 02:26:01 GMT

19 серия культового соревнования начнётся в пятницу, 5 августа, в 0:00 UTC.

ICFP Programming Contest — международное соревнование по программированию, проводимое ежегодно летом с 1998 года. Результаты соревнования объявляются на Международной конференции по функциональному программированию. (с) Wikipedia

Читать дальше →