В рейтинге участвует:

групп:

каналов:

Виртуальный сервер на SSD - недорого!

Аренда выделенных и виртуальных серверов (VDS/VPS), хостинг, аренда IP-адресов, администрирование, круглосуточная поддержка

qwarta.ru подробнее

Резервное копирование с проверкой на вирусы!!!

Удобный сервис создания резервных копий на любой сервер сети интернет. Отслеживайте изменения, проверяйте на вирусы. Надежно защитите свой бизнес!

go.backupland.com

Выбираете сервер? Любая конфигурация на заказ!

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

qwarta.ru подробнее

Size: a a a

Infernal Math

413 membersпожаловаться на группу
2021 July 15

X

Xak in Infernal Math
да не, пока я чисто для интереса разбираюсь в языке, проект пока даже не начался. Я очень даже не жалуюсь на жизнь  (особенно если делить доход на времязатраты). Это скорее недовольство тем, что инструмент несовершенен в тех аспектах, в которых уже давно пора бы НЕ
источник
01:21пожаловаться#1

X

Xak in Infernal Math
со скалой трудно сравнить, в общем. Скала всё-таки серьёзный промышленный язык
источник
01:21пожаловаться#2

A

Andrey in Infernal Math
Так может ты просто не тот язык тыкаешь?
источник
01:22пожаловаться#3

L

Lena in Infernal Math
Тут есть два пути: либо впрягаться и показывать посонам, как на самом деле делаются дела, либо забить. Либо запилить свой язык, как Гвидо ван Поссум или как там его звали...
источник
01:22пожаловаться#4

X

Xak in Infernal Math
может быть. Надо посмотреть, где ещё есть верификация в похожем на F* ключе
источник
01:22пожаловаться#5

X

Xak in Infernal Math
там, к сожалению, почти везде всё "не очень"
источник
01:23пожаловаться#6

A

Andrey in Infernal Math
Так если он противный, зачем искать похожие?)
источник
01:23пожаловаться#7

X

Xak in Infernal Math
нет, я имею в виду похожий по способу взаимодействия с прувером
источник
01:23пожаловаться#8

X

Xak in Infernal Math
основной месседж этого языка:
Вам больше не нужны тесты. Ваша программа не скомпилится без доказательства корректности ваших функций
источник
01:24пожаловаться#9

X

Xak in Infernal Math
мне в некотором смысле нравится этот месседж
источник
01:24пожаловаться#10

A

Andrey in Infernal Math
В Idris что-то похожее делают
источник
01:25пожаловаться#11

X

Xak in Infernal Math
я прекрасно понимаю, что дьявол в деталях и правильных формулировках корректности не меньше, чем в самих доказательствах
источник
01:25пожаловаться#12

X

Xak in Infernal Math
но мысль хороша
источник
01:25пожаловаться#13

A

Andrey in Infernal Math
Хотя честно говоря кажется, что удобно доказывать корректность программ ещё нигде не научились
источник
01:25пожаловаться#14

X

Xak in Infernal Math
и я начал потихоньку настукивать на этом языке систему типов абстрактной алгебры
источник
01:25пожаловаться#15

A

Andrey in Infernal Math
Везде извороты какие-то
источник
01:25пожаловаться#16

X

Xak in Infernal Math
в принципе, добрался от полугрупп и колец до PID, доказал, что Z — PID, и прувер Z3 одобрил моё доказательство
источник
01:26пожаловаться#17

X

Xak in Infernal Math
дальше полез и упёрся в то, что для пользовательских типов нельзя отношение эквивалентности (==) переопределить, и стал переправлять все свои определения со встроенного на своё отношение eq, попутно введя все нужные термины (бинарное отношение, рефлексивность, симметричность, транзитивность)
источник
01:27пожаловаться#18

A

Andrey in Infernal Math
"Математические" вещи, кажется, лучше в Lean, Isabelle/HOL или Coq доказывать
источник
01:28пожаловаться#19

X

Xak in Infernal Math
соответственно если всё пойдёт нормально — сконструирую общие дроби, потом пойдут всякие нужные в алгебре конструкции — поле частных, многочлены над полем, матрицы и пр.
источник
01:28пожаловаться#20