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

Взлом 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, должен проявлять себя при каждом запуске в том же месте кода.
Читать дальше →

Формальная верификация кода на 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), а именно, мы затронем следующие темы:

[Перевод] Сравнение одинакового проекта в 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, но у них оказалось в три раза больше кода из-за разных дизайнерских решений. В конце концов, самая большая разница в количестве кода оказалась в пределах одного языка!
Читать дальше →

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 и насколько это просто.
Продолжение

[Перевод] Сегфолт в glibc, 345 тысяч утёкших сокетов и 474 тысячи соединений за полминуты: шесть багов в одной цепочке

opium — Mon, 19 Oct 2026 04:01:37 GMT

Плановые работы в сети раз за разом валили процессы Kafka: segfault в DNS-резолвере glibc, сотни тысяч утёкших UDP-сокетов, полмиллиона TCP-соединений за 31 секунду после восстановления. Инженер Jane Street разматывает цепочку из шести багов (два из них старше десяти лет): как нашли причину, какие числа подтвердили гипотезу и чем всё закрыли.

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

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

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

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

Как сделать 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

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

[Перевод] Пишем эмулятор Game Boy на OCaml

PatientZero — Fri, 14 Jan 2022 07:51:16 GMT

Введение

Последние несколько месяцев я работал над проектом под названием CAMLBOY — эмулятором Game Boy, написанным на OCaml, который работает в браузере. Протестировать его можно на следующей странице демо:

Страница демо

Я добавил в демо несколько неофициальных ROM, поэтому в них можно поиграть (рекомендую Bouncing ball и Rocket Man Demo). Также можно поиграть в них в мобильном браузере, на современных смартфонах эмулятор работает с частотой 60 FPS.

Репозиторий

Репозиторий находится здесь:

https://github.com/linoscope/CAMLBOY
Читать дальше →

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 исправлен). О том, что было сделано, и как с этим жить, читайте под катом. Мне интересно.

Реализация расширения Active Patterns для языка OCaml

JetBrains_Education (Образовательные проекты JetBrains) — Mon, 05 Oct 2020 16:57:58 GMT

О проекте

Весной 2020 года в рамках весенней практики в Computer Science Center я занимался разработкой новой конструкции для языка программирования OCaml под чутким руководством Дмитрия Косарева.

Почему OCaml

OCaml – это одна из самых успешных и развитых реализаций синкретизма промышленного программирования (отсюда мультипарадигмальность, мультиплатформенность, очень быстрый компилятор, высокая производительность генерируемого кода) и математики (отсюда state-of-the-art система типов с мощной реализацией вывода типов, выразительность и расширяемость языка, близость к математической нотации и семантике).

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

Для более глубокого погружения в тему предлагаю взглянуть на статьи OCaml for the masses и Why OCaml.

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

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 и RESTful JSON API с использованием Eliom

nbytes — Thu, 24 Aug 2017 15:19:23 GMT

Привет, Хабр! Представляю вашему вниманию перевод руководства RESTful JSON API using Eliom.

В этом руководстве рассказывается, как создать простой, но полный REST API с использованием JSON в качестве формата сериализации.
Читать дальше →

Приглашаем на конференцию FPConf 2017

vorona_karabuta (RubyRussia) — Fri, 03 Nov 2017 19:32:48 GMT

Привет!

2 декабря ждем всех, кто любит делать это функционально на третьей конференции FPConf — конференции о Haskell, Scala, Clojure, Elixir, Kotlin, F# и функциональных подходах в программировании фронтендов, бэкендов и чего угодно на чем угодно. Больше монад, лямбд, замыканий! Всем иммутабельность, друзья :)

Традиционно, приглашаем как опытных функциональщиков, так и тех, кто только хочет получить вдохновение и расширить горизонты.

Цена билета сейчас — 5000 рублей. Регистрация тут.

Что в программе:

Arnaud Spiwack, core-разработчик Coq Proof Assistant, старший архитектор в Tweag I/O

USING HASKELL TO GREAT EFFECT

It is beyond cliché, nowadays, to say that testing is really important. This is even more so in I/O intensive applications because so many things can go wrong. Unfortunately, testing I/O intensive applications is particularly hard. We have to mock all our files, data-bases, and so on. But even so, we're only scratching the surface: so many things can go wrong. How do we test for absence of deadlocks? Of races?

I came to the conclusion that Haskell's insistence on purity made it, paradoxically, one of the best languages to write I/O intensive programs. The reason for this is that Haskell makes it very easy to mock every single aspects of the I/O fabric, hence testing is more powerful. Up to checking for the absence of deadlocks and races. This talk will discuss the programming patterns which emerge from this point of view, and, of course, encourage you do use them in your programs.
Смотреть всю программу