Функциональное программирование *

Статья предполагает, что читатель имеет опыт работы с интерактивным программным средством доказательства теорем — Coq.

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

В данной статье мы рассмотрим прием, который используется для работы с рекурсивными функциями, которые не проходят проверку завершаемости (тотальности) в Coq. Под «горючим» мы будем понимать натуральное число, которое вводится как дополнительный параметр в тело функции, чтобы обозначить верхнюю границу числа итераций, которые функция может совершить. Таким образом функция трансформируется в завершаемую, удобную для работы, и радушно принимаемую компилятором Coq. В литературе термин встречается под названиями: petrol, fuel, gas и т.д.

Положим, перед нами стоит задача: необходимо верифицировать функцию, написанную на каком-либо языке программирования. Мы разбираемся в том, что делает эта функция, уже прикидываем, какие леммы сформулируем, чтобы доказать, что она ведет себя именно так как ожидается. Переводим функцию на Coq (вручную, или с помощью автоматических переводчиков, если только таковые имеются для требуемого языка), и видим, что проверка Coq на завершаемость нашей функции (termination check) провалилась.

Это значит Coq не может определить какой аргумент на каждом шаге итерации будет уменьшаться. Можно попробовать явно указать Coq на аргумент, который, мы точно знаем будет уменьшаться на каждом шаге {struct уменьшаемый_аргумент}:

Данная статья является адаптированной русскоязычной версией моей статьи: Handling fold_left in proofs.

Функция fold_left , сворачивающая список, довольно популярна во многих (функциональных и не очень) языках программирования. Она есть и в Haskell, и в OCaml и в Rust. Используется чаще, чем fold_right, вероятно потому, что с ее помощью проще писать эффективный код.

fold_left и fold_right из библиотеки OCaml library: List.

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

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

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

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

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

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

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

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

Совсем недавно команда разработки Dart выпустила 3-ю версию языка, которая привнесла много новых крутых штук и возможностей. Одним из нововведений стали модификаторы классов, которые довольно сильно расширили выразительные возможности Dart. С одной стороны, новые модификаторы ложатся в стройную картину и даже логичны; с другой - чувствуется некоторая многословность ( abstract interface class вместо общепринятого interface) и появление ряда ограничений, которых ранее не было. Новые модификаторы классов безусловно интересны и требуют внимания, но сегодня мы будем говорить не о них). Оставим уже вышедшие модификаторы для одной из следующих статей. Логично задаться вопросом: о чем тогда сейчас пойдет речь? Заинтригованы? Тогда добро пожаловать под кат.

Привет, хабр!

Данная задача в разных вариациях мне давалась на нескольких собеседованиях несколько лет назад. Хоть мой дизайн и проходил, мне стало интересно реализовать это в коде с нуля. Сыроватый и сильно урезанный по функционалу MVP готов, ссылка на github будет под катом. Пока что мной запланировано 3 статьи - эта, по бэкенду и по фронту. Будет много кода на scala, много котов (cats effect), стримов (fs2), пара lock-free техник, scala js, и постараюсь сделать так, чтобы мозг от всего этого не взорвался.

Все, кому интересно - добро пожаловать под кат.

Привет! Меня зовут Сергей Грибков, я тимлид команды FM&RA в билайне, и в этом посте я хочу рассказать об одной фирменной особенности Scala под названием implicits. Это неявные параметры, неявные преобразования, неявные классы.

Почему неявные — потому что они не требуют прямого вызова, если мы говорим о методах, не требуют прямой передачи в метод, если мы говорим о параметрах, и так далее.

В Scala implicits широко распространены. Скорее всего, вы уже сталкивались с ними в различных библиотеках и фреймворках, например, Apache Spark. 

Чтобы успешно использовать implicits в собственном коде и работать со сторонними библиотеками, требуется понимание принципов их работы. Поэтому давайте разберем, как всё устроено.

Итак, существует три основных категории implicits:

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

Сводится ли к конечному автомату человеческий интеллект? К сожалению, у человеческого интеллекта есть атрибут, природа которого современной науке неизвестна и который никогда не наблюдался у конечных автоматов, например у арифмометра. Этот атрибут - ощущение собственного "я", self-awareness. Конечно вы можете сделать в программе переменную "я_чувствую_собственное_я" и присвоить ей true, а потом утверждать, что вы симулируете собственное "я", но это жульничество, а не технология.

Я вовсе не пытаюсь нагонять мистику или агитировать за бога. Self-awareness наверняка такой же физический феномен, как какая-нибудь термоядерная реакция. Но скажем древние греки не знали природы термоядерной реакции. Наверное, они вели диалоги типа "если ты не веришь, что Солнце - просто большой костер из дров, то значит ты веришь в сказки про Зевса и других богов?"

Если бы Достоевский жил в наше время, смотрел по вечерам «Черное зеркало» и просто читал новости, то, скорее всего, Раскольникова судил бы Искусственный интеллект.

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

Привет, Хабр, это команда  Alliesverse – платформы для управления бизнесом – и это в наши воспаленные мозги попала идея о современном Раскольникове...
Случилось это на большом мероприятии, посвященному ChatGPT, на которое нас пригласили. Мы подумали: а что если ускорить наступление высокотехнологичного и справедливого суда и попробовать обучить ИИ всем российским кодексам ?

Так сформировался эмбрион LawAi by Alliesverse. Под катом, подобно ChatGPT, расскажем наш опыт обучения русскоязычных и зарубежных моделей нейросетей российскому законодательству.

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

Спойлер х2: использование ChatGPT, Notion и прочих готовых решений не подходит для создания юрисконсульта в кармане, т.к. они обучаются на международном массиве данных, у которого много расхождений с российским законодательством.

Привет! Меня зовут Никита Калинский, я разработчик в Тинькофф Бизнесе. Сейчас я занимаюсь продуктом под названием «Лента операций». Физлица в желтом приложении могут отслеживать все свои операции, и мы делаем такой же инструмент для предпринимателей.

Сегодня я хочу поговорить про основы различных систем исполнения эффектов в Scala. Мы разберем, как работают системы эффектов, как они реализованы в Scala в Cats Effects и ZIO и как эволюционировали между версиями. А также обсудим неявные особенности и подводные камни исполнения сред таких библиотек.

Заявление звучит довольно громко и, я бы даже сказал, провокационно. Но в последние годы я всё больше и больше считаю, что это утверждение действительно верно, и хочу подробно объяснить, почему.

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

Новый план состоит в том, чтобы использовать синтаксис Elixir как он есть (да!) Ну, разве что, типы в него добавить. Также, нужно сделать соответствие модулей и физических файлов 1:1.

UPDATE: berry будет поддерживать макросы, но только импортируемые. use поддерживаться не будет.

import Ecto, macros: [from]

Таким образом, фанатам Ecto беспокоиться не о чём. Вы хотите спросить, не хочу ли я поделиться этой идеей с более широким сообществом? Я уже сделал это! А вот, какая была реакция - об этом читайте под катом.

В викенд я зашел в кафе Red Rock и встретил там программистку встроенных систем Машу Горбунову. Вообще, у этого кафе в Маунин-Вью, Калифорния можно встретить кого угодно - например однажды на меня прямо из-за угла вылетел основатель Гугла Сергей Брин. Так вот Маша рассказала мне что программирует RTOS (семафоры, мейлбоксы, сигналы), чему выучилась в свое время в питерском институте ГУАП (аэрокосмического приборостроения).

Я решил, что такая девушка не должна оставаться в другой отрасли и показал ей плату ПЛИС, внутри которого можно засинтезировать пару ядер ARM микроконтроллерного класса. На что Маша среагировала так (видео):

Привет! Сегодня хочу поделиться идеей нового языка для платформы BEAM: читатели хабра всё должны узнавать из первых рук! Планируется, что он будет транслироваться в эрланг source-to-source, и семантически будет тоже максимально совместим с эрлангом.

berry-lang поддерживает статическую типизацию, однако типы в нём - не главное. Главное - это приятный синтаксис, о чём свидетельствует его ягодное название. Кстати, о названии: помимо того, что оно созвучно слову Erlang, у него есть и другая подоплёка.

Дело в том, что berry-lang крадёт весь свой синтаксис у языка Сyber (слышали о таком?) Получается - кибер-тема. А чем заняты в кибер-городе? Выращиванием ягод, конечно! Скриншот - из последней Матрицы, на нём генерал Найоби угощает Нео клубникой и говорит, не без гордости - "Zion could have never made something like this!".

Статья содержит много коротких примеров с кодом! Будет интересна всем поклонникам языка эрланг и платформы BEAM. А если о языке Сyber ничего не слышали, то вообще - must-see.

В заметке Ричарда Тауэрса (Richard Towers) Typescripting the technical interview (есть перевод на Хабре: Руны и лёд: техническое собеседование по TypeScript) по ходу повествования была решена классическая задача расстановки 8 ферзей на шахматной доске. Для решения использовалась система типов TypeScript. Мне захотелось посмотреть, как эта задача будет выглядеть на Scala. Т.к. Scala 3 помимо развитой системы типов предлагает превосходную поддержку метапрограммирования, то здесь мы рассмотрим не только решение на типах, но и мета-программное решение.