DV
насчет памяти на яве и плюсах - ой, много у меня на этот счет есть что сказать, со слезами на глазах ...
Size: a a a
2021 April 28
B
Говорите
ДК
А где эту базу глянуть?
DV
Ссылка на архив: http://us.metamath.org/downloads/metamath.tar.bz2
B
Теперь вопрос
DV
про память - попробую вкратце. Несмотря на то, что якобы философия с++ позволяет не платить за то, что не используется, в реальности попытка написать "эффективную" программу приводит к плохим последствиям в силу той архитектуры системы, которую навязывает императивщина. Сейчас, если бы я опять начал писать на плюсах, я бы имитировал функциональщину как можно ближе и как можно чище.
B
Каким образом сделаете верификацию russell?
B
Функциональное программирование далеко от архитектуры компьютера. Функциональный код трудно оптимизировать.
DV
Вопрос хороший, но вначале надо сделать систему верификации для flow9, на котором russell написан, после этого можно уже формально верифицировать и самого рассела, и компилятор flow9, который написан на flow9.
AT
StrictData go brrrrr.... 😂
DV
Спорное утверждение. То, чо ФП далеко от железа - это понятно, но вот оптмизации - это дело такое. Можно делать микрооптимизации на несколько инструкций - это позволяет как раз близость к железу, а можно например в хвост и в гриву использовать параллельность, что довольно легко в чистом коде - это даст хороший выигрыш при минимальных усилиях (ну если уметь, конечно. Я вот все учусь, но есть успехи)
ДК
А в более человекопонятном виде это есть?
DV
Если вы имеете в виду доказательства - то нет. Вообще метамат - это аналог машинного языка для представления доказательств, для того,чтобы понять что там такое нужны внешние инструменты - программы, которые все это разберут и покажут и человеческом виде. Ну сам метамат как программа например
DV
Я собссна свой проект начал потому что метамат меня вдохновил как низкоуровневый, но супер выразительный язык, но вот человеческого интерфейса к нему не хватает
ДК
Да хотя бы просто наглядное представление аксиом/теорем, без самих доказательств.
DV
Вот правило вывода modus ponens
s
Популярное заблуждение.
s
См. "SSA is functional programming", ANF, etc.
DV
ой, сорри, это не modus ponens, это какая то простая теоремка из двух применений modus ponens
DF
Все равно выглядит забористо