Follow

Все же не зря мы в универе изучали конечные автоматы...это конечно только способ формальной записи по сути, но какой удобный.

@3draven Это после изучения Erlang/Elixir такая реакция?

@kirillgrachoff нет, просто в голову пришло.

@3draven а, понял.

Думал, из-за того, что код в акторах (которые по сути стейт машины с состоянием) выглядит компактно и хорошо скейлится. Я просто словил катарсис, когда понял, как это просто.

@kirillgrachoff это немного упрощенный взгляд на конечные автоматы, сам по себе эрланговский процесс не является таковым из коробки

@3draven

@mudasobwa @3draven
На чистом Erlang не писал. Не разбираюсь.

В Elixir всё очень похоже.

@kirillgrachoff эликсир — это набор макросов над эрлангом, он выполняется на эрланговой виртуальной машине и процессы в нем чисто эрланговские.

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

Моя библиотека hexdocs.pm/finitomata — немного приближает процессы к настоящему конечному автомату (persistency layer и гарантии защиты от плохого клинентского кода).

@3draven

@mudasobwa

Понял. Не зал подробностей (не задумывался про hypervisor и перезапуск). Да, действительно ломает. (Надо бы, наверное, где-то найти длинный email почитать про то, почему перезапуск в начальном состоянии, а не в последнем корректном. Догадка состоит в том, что оно упадёт точно так же)

Не уверен, что посмотрю библиотеку, но кажется, что это правильный шаг. (особенно если там где-то есть консенсус)

@3draven

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

Консенсус для правильной реализации конечного автомата не нужен, это другая задача.

@3draven

@mudasobwa

Понял. (бенчмаркам верить можно)

Да, можно обойтись выбором лидера (что эквивалентно консенсусу с точки зрения математики).
Здесь вопрос в том, как понять, что процесс умер, и надо начать принимать модификации состояния от другого процесса (и от какого).
А. Или Erlang VM как-то сама занимается поднятием ровно 1 процесса на замену каждому процессу на упавшей машине?

@3draven

@kirillgrachoff какого еще лидера? Там нет лидеров, это другая задача, сказал же.

@3draven

@kirillgrachoff

> Не уверен, что посмотрю библиотеку

А зачем на нее смотреть? Принцип работы я описал, а код вы скорее всего не поймете.

@3draven

@3draven конечные автоматы обеспечивают математически доказанную гарантию консистентности, но, к сожалению, даже Хаскель не позволяет эту гарантию перенести в машинный код.

Я не случайно прототип своей библиотеки FSM писал на Идрисе.

@mudasobwa если ты споришь, то неясно с чем. Если нет, ну, ок. Они не настолько хитрая штука что бы спорить.

@3draven «конечный автомат — это просто форма записи» примерно такого же уровня утверждение, как «чисел меньше нуля не бывает». В четвертом классе ждут сюрпризы.

Регулярные выражения тотальны (заканчиваются за конечное время) — только благодаря математике конечных автоматов, иначе их нельзя было бы использовать в принципе: любая регулярка могла бы вгонять код в бесконечный цикл. Таких примеров вагон.

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

@3draven этот способ записи, реализованный на Idris, Agda,или Coq, в отличие от всех остальных языков, позволит формально доказать правильность реализации. Тесты будут не нужны.

Sign in to participate in the conversation
MustUdon

I like Twitter, but, Mastodon it is so excited! Feel free to register it is server just for fun! Usefull links https://instances.social https://www.reddit.com/r/Mastodon/comments/yugh2o/some_useful_mastodon_lists/?utm_source=share&utm_medium=web2x&context=3