[07:23:04] <ada_ru> (Eugene)  отвечает (I_vlxy_I) на <Точнее даже так: Com…>
И все три на основе виртовского коммилятора 80-х годов...
[10:19:52] <ada_ru> (I_vlxy_I)  отвечает (Eugene) на <И все три на основе …>
AO вроде уже нет
[10:20:32] <ada_ru> (I_vlxy_I) По крайней мере там уже сильно другой компиль
[10:24:14] <ada_ru> (Борис) OP2, на основе которого большая часть компиляторов Оберона сделано, это тоже не виртовский. Школа таже, но компилятор не тот, что писал Вирт в 80-х.
[10:30:38] <ada_ru> (Борис) «Тот самый» компилятор, в модернизированном виде, входит сейчас в Project Oberon 2013. Ну и в те компиляторы O7, которые от него происходят.
[10:40:15] <ada_ru> (I_vlxy_I) короче, ошибки в них будут скорее всего разные
[10:40:17] <ada_ru> (I_vlxy_I) и это хорошо
[11:46:42] <ada_ru> (Eugene)  отвечает (I_vlxy_I) на <и это хорошо>
Ошибок вообще не должно быть, но с оберонами это невозможно из-за отсутствия формального определения языка...
[11:47:38] <ada_ru> (Eugene)  отвечает (I_vlxy_I) на <По крайней мере там …>
Там вроде два компилятора, один (новый) с нуля написан...
[11:49:46] <ada_ru> (I_vlxy_I)  отвечает (Eugene) на <Ошибок вообще не дол…>
Ошибки всегда были, есть и будут. Проектировать систему исходя из предположения, что в ней не будет ошибок - ошибка
[11:49:48] <ada_ru> (Eugene) Эксельсиоровцы, сделавшие когда-то топовый компилятор оберона/2-модулы/2, вообще на скалу перешли...
[11:52:36] <ada_ru> (Eugene)  отвечает (I_vlxy_I) на <Ошибки всегда были, …>
По крайней мере, формальная верификация гарантирует отсутствие ошибок в реализации модели ПО. Остаются лишь ошибки в самой модели...
[11:54:28] <ada_ru> (I_vlxy_I) Считай, что реализация на ЯП это и есть модель, таким образом в реализации ошибок нет! Есть только в модели.
[11:55:09] <ada_ru> (Eugene) А чертёж самолёта и есть самолёт!!!
[12:06:22] <ada_ru> (I_vlxy_I) ну, в принципе да, если по чертежу компилятор автоматом этот самолет напечатает например.
[12:50:16] <ada_ru> (Eugene) Ну  и вот, в компиляторе могут быть баги, патамушта непонятно, как правильно компилировать, ведь нет формального описания языка. Без внятного тз результат хз...
[13:08:11] <ada_ru> (I_vlxy_I) Код компилятора и есть формальное описание
[13:11:44] <ada_ru> (nitrocerber) А днк - формальное описание челавекаф. Тока его нормально до сих пор никто не расшифровал
[13:11:48] <ada_ru> (nitrocerber) Так что такая себе модель
[13:13:51] <ada_ru> (I_vlxy_I)  отвечает (nitrocerber) на <А днк - формальное о…>
Ну, кстати, в ДНК содержится не вся информация о человеке.
[13:15:19] <ada_ru> (I_vlxy_I) Если мы нашли днк человека и ничего больше о этом виде приматов не знаем и не знаем даже что такое приматы, то полностью однозначно реконструировать человека, как вид, просто так не получится.
[13:35:39] <ada_ru> (Максим) почему?
[13:36:57] <ada_ru> (nitrocerber) Та ну, синиезируешь белок, фигачишь его в инкубатор, выращиваешь его, б-ть. С генной инженериешь зашибичь
[13:39:34] <ada_ru> (I_vlxy_I)  отвечает (Максим) на <почему?>
Потому, что на формирование эмбриона оказывает влияние и среда в которой он находится.
[13:40:06] <ada_ru> (I_vlxy_I) Там такое.. рекурсивное.
[13:40:31] <ada_ru> (I_vlxy_I) И все механизмы ещё не изучены. Механизмы эмбриогенеза.
[13:41:44] <ada_ru> (I_vlxy_I) Вообще легко может оказаться что человеческий эмбрион нормально не развивается без какого-нибудь вируса, что живет в его мамке
[17:53:41] <ada_ru> (Eugene) www.popmech.ru/science/news-460412-zachem-v-sibiri-vyrashchivayut-chelovecheskie-mozgi/
интересно, зачем?
[17:54:53] <ada_ru> (Eugene)  отвечает (I_vlxy_I) на <Код компилятора и ес…>
разве что какого-то диалекта этого языка, причём диалекта формально не описанного нигде
[18:00:20] <ada_ru> (Борис)  отвечает (Eugene) на <Ну  и вот, в компиля…>
Почему нет?
[18:00:50] <ada_ru> (I_vlxy_I) формальное == машиночитаемое, скорее всего.
[18:01:17] <ada_ru> (Eugene)  отвечает (Борис) на <Почему нет формально…>
а где оно? то, что написал Вирт в 17 страничках — это неформальное описание
[18:01:43] <ada_ru> (Борис)  отвечает (I_vlxy_I) на <формальное == машино…>
EBNF вполне машиночитаем.
[18:01:49] <ada_ru> (Eugene)  отвечает (I_vlxy_I) на <формальное == машино…>
формальное — это такое, по которому можно потом математически верифицировать реализацию
[18:01:53] <ada_ru> (I_vlxy_I) EBNF это не описание языка
[18:01:57] <ada_ru> (I_vlxy_I) это лишь его грамматика.
[18:02:15] <ada_ru> (Борис) Да, тогда у какого языка есть у нас формальное описание?
[18:02:28] <ada_ru> (I_vlxy_I) вроде у подмножества Си есть например.
[18:02:29] <ada_ru> (Борис) Чтобы верифицировать.
[18:02:37] <ada_ru> (I_vlxy_I) тут ссылки пролетали
[18:02:45] <ada_ru> (Борис) Подмножество это не весь язык.
[18:02:54] <ada_ru> (Eugene)  отвечает (Борис) на <EBNF вполне машиночи…>
ЕБНФ — это всего лишь синтаксис, да и то в виртовском ЕБНФ есть дыры с теми же пробелами вокруг ключевых слов
Семантика в ЕБНФ вообще никак не отражается
[18:02:57] <ada_ru> (I_vlxy_I) подмножество само по себе - язык.
[18:03:02] <ada_ru> (I_vlxy_I) полноценный.
[18:03:19] <ada_ru> (Борис)  отвечает (Eugene) на <ЕБНФ — это всего лиш…>
Там кроме Вирта ещё несколько языков есть.
[18:03:44] <ada_ru> (Eugene)  отвечает (Борис) на <Да, тогда у какого я…>
CakeML имеет формально-верицицированный компилятор, CompCert — компилятор подмножества Си
[18:03:55] <ada_ru> (Борис)  отвечает (I_vlxy_I) на <полноценный.>
Не придирайся к словам. Я про язык целиком. Типа Си++98
[18:04:24] <ada_ru> (Борис)  отвечает (Eugene) на <CakeML имеет формаль…>
Два языка? А сколько не имеют? Ада имеет?
[18:05:11] <ada_ru> (Борис) Представьте себе формальное описание С++20, по которому можно проверить компилятор.
[18:05:15] <ada_ru> (Eugene) В си есть вещи, которые трудно формализовать — типа stjump-longjump и переменное количество параметров в функциях, их выкинули из подмножества, реализованного в CompCert
[18:06:54] <ada_ru> (Eugene)  отвечает (Борис) на <Два языка? А сколько…>
вот ещё какая-то Люстра: https://www.researchgate.net/publication/319856100_A_formally_verified_compiler_for_Lustre
[18:06:58] <ada_ru> (I_vlxy_I) Борис ты спрашивал про языки для которых есть формальное описание. тебе привели примеры и языков и описаний и реализаций. Да, это не Си и не С++. Но это языки.
[18:07:04] <ada_ru> (Борис) Оберон проще формализовать в этом смысле. Вот этим специально никто не занимался — да. Но среди промышленных (применяемых) нет просто языков с формальным описанием (в этом смысле) и тем более с верифицированным компилятором. Это печально, да.
[18:07:20] <ada_ru> (I_vlxy_I) Оберон же, или его подмножество, пока никто не формализовал.
[18:07:24] <ada_ru> (Eugene)  отвечает (Борис) на <Два языка? А сколько…>
У ады нет формального описания, поэтому адские компиляторы и приходится проверять тысячами тестов
[18:07:25] <ada_ru> (I_vlxy_I) об этом речь.
[18:07:35] <ada_ru> (I_vlxy_I) А вообще, с оберонами можно пойти на @oberonf и там обсудить.
[18:08:05] <ada_ru> (Eugene)  отвечает (I_vlxy_I) на <А вообще, с оберонам…>
так тот чат не по оберону, а по форуму про ББЦБ
[18:08:06] <ada_ru> (Максим) 🚀  О, ракеты на Аде! Класс https://www.hackster.io/laetitiael/superimu-circle-an-adaimu-9f1151
[18:08:33] <ada_ru> (Борис)  отвечает (Eugene) на <так тот чат не по об…>
Он вообще чат.
[18:08:53] <ada_ru> (Eugene)  отвечает (Борис) на <Он вообще чат проект…>
какого проекта?
[18:09:54] <ada_ru> (I_vlxy_I)  отвечает (Максим) на <🚀  О, ракеты на Аде!…>
"ISP port" — это что такое? SPI знаю, I2C знаю, ISP не знаю.
[18:10:19] <ada_ru> (Борис)  отвечает (I_vlxy_I) на <А вообще, с оберонам…>
Удивительная реакция Алексей. :) Самому регулярно накидывать здесь — пожалуйста, а так лучше пойти... :)
[18:10:47] <ada_ru> (Борис) Так то я согласен полностью, нехрен забивать чат по другому языку)
[18:10:50] <ada_ru> (I_vlxy_I)  отвечает (Борис) на <Удивительная реакция…>
дык я же что? я за то, чтобы другие заинтересованные в формальном обероне тоже могли прочитать и поучаствовать.
[18:10:56] <ada_ru> (I_vlxy_I) тут их как бы нету.
[18:11:15] <ada_ru> (Eugene)  отвечает (Борис) на <Представьте себе фор…>
был бы оберон настолько же большим и сложным, как современный с++, я бы даже и упоминать про его формальное описание не стал бы...
[18:11:20] <ada_ru> (Максим) > For someone, like me, who is used to C/C++ and java environment, it wasn't exceptionnaly hard to put the hand on the Ada. Specially that it reminds me Pascal and Caml that I used in very past.
[18:11:53] <ada_ru> (I_vlxy_I) недавно смотрел какой-то кусок на каком-то паскале. насколько же Ада отличается! в лучшую сторону.
[18:12:16] <ada_ru> (Eugene)  отвечает (Максим) на <> For someone, like …>
ада как бы совсем не похожа на камл
[18:12:18] <ada_ru> (I_vlxy_I) ну или паскалисты просто забивают на адекватное оформление своих исходников, я хз
[18:14:23] <ada_ru> (Eugene)  отвечает (I_vlxy_I) на <дык я же что? я за т…>
сомневаюсь, что там найдётся кто-то, кто захочет формализовать описание оберона
да и какого именно из оберонов? развели кучу малу, хрен разберёшься...
[18:14:25] <ada_ru> (I_vlxy_I)  отвечает (Максим) на <🚀  О, ракеты на Аде!…>
таки да, у чела там опечатка вначале. не ISP а SPI.
[18:14:54] <ada_ru> (Eugene) ISP — интернет сервис провайдер, чо непонятного???
[18:15:24] <ada_ru> (I_vlxy_I)  отвечает (Eugene) на <сомневаюсь, что там …>
я бы начал с "Oberon-7" точнее уже Oberon-16, по факту.
[18:17:11] <ada_ru> (Eugene)  отвечает (I_vlxy_I) на <я бы начал с "Oberon…>
предлагаю его называть просто Oberon, как это делает автор языка
[18:17:51] <ada_ru> (I_vlxy_I) Вот тут ( https://www.inf.ethz.ch/personal/wirth/Oberon/index.html ) документ называется The Programming Language Oberon-07 (Revised Oberon)
[18:18:05] <ada_ru> (I_vlxy_I) то есть всё сложно
[18:18:19] <ada_ru> (Максим) Может вам и правда со своим обероном пойти куда-то
[18:18:35] <ada_ru> (Eugene)  отвечает (I_vlxy_I) на <Вот тут ( https://ww…>
The Programming Language Oberon
Revision 1.10.2013 / 3.5.2016
Niklaus Wirth
https://www.inf.ethz.ch/personal/wirth/Oberon/Oberon07.Report.pdf
[18:18:52] <ada_ru> (Eugene)  отвечает (Максим) на <Может вам и правда с…>
но ведь оберон — это микроада!!!
[18:18:58] <ada_ru> (Eugene) даже наноада
[18:19:32] <ada_ru> (I_vlxy_I)  отвечает (Eugene) на <даже наноада>
обоснуй
[18:20:01] <ada_ru> (Eugene)  отвечает (I_vlxy_I) на <обоснуй>
ну он же наноразмеров, а призван решать те же задачи, что и ада
[18:20:46] <ada_ru> (Eugene) модули — есть, расширяемые записи — есть, минимальный набор управляющих конструкций — есть
[18:21:09] <ada_ru> (I_vlxy_I)  отвечает (Eugene) на <ну он же наноразмеро…>
Оберон, изначально, пилился как язык для GUI-системы. Антиреалтаймовой, так сказать. Со сборщиком мусора и прочими приколами. То есть в плане назначения Оберон в чем-то даже ближе к js нежели к Аде.
[18:21:38] <ada_ru> (Eugene) да нету никакого сборщика мусора и GUI в описании языка, это всё твои измышлизиы
[18:22:15] <ada_ru> (I_vlxy_I)  отвечает (Eugene) на <да нету никакого сбо…>
Ой, всё.
[18:22:17] <ada_ru> (Максим) Народ сюда про Аду приходит почитать, а тут как не С++, так Оберон, если не криптовалюты 😕
[18:22:30] <ada_ru> (Борис) Вот да
[18:22:42] <ada_ru> (Eugene) или вовсе какое-то там генетическое программирование
[18:22:58] <ada_ru> (Eugene) админ — флудер!!!
[18:23:10] <ada_ru> (Борис)  отвечает (Eugene) на <админ — флудер!!!>
Да ещё какой.
[18:24:08] <ada_ru> (I_vlxy_I) Максим А не знаешь, чем он там исходники красил? Там явно какой-то текстовый редактор с лексической раскраской. Или около того.
[18:24:24] <ada_ru> (I_vlxy_I) картинка https://www.ada-ru.org/files/bot/2019-01-29-x1.jpg
[18:24:41] <ada_ru> (Eugene) vscode detected
[18:25:08] <ada_ru> (Eugene) хотя может и GPS
[18:25:49] <ada_ru> (Максим) Ну на других скриншотах там точно GPS
[18:25:58] <ada_ru> (I_vlxy_I) а это не скриншот
[18:26:06] <ada_ru> (I_vlxy_I) это ТЕКСТ
[18:26:15] <ada_ru> (I_vlxy_I) то есть он выделяется в браузере. ну и в DOM видно
[18:26:55] <ada_ru> (I_vlxy_I) и слова там помечены классами - кейворд или не кейворд например.
[18:27:13] <ada_ru> (Максим) может движок Hackster?
[18:27:43] <ada_ru> (I_vlxy_I) А вот тут видно, что движок немного попутал
[18:27:46] <ada_ru> (I_vlxy_I) картинка https://www.ada-ru.org/files/bot/2019-01-29-x2.jpg
[18:27:55] <ada_ru> (I_vlxy_I) и покрасил ключевые слова в комментах 😊
[18:29:26] <ada_ru> (Eugene)  отвечает (I_vlxy_I) на <это ТЕКСТ>
был редактор Context, там можно настраивать раскраску синтаксиса и потом экспортировать в html-код выделенный текст, я так когда-то баловался, хаскельные проги для ЖЖ раскрашивал
[18:30:54] <ada_ru> (Максим) ну в том же libadalang есть раскрасчик в HTML в примерах
[18:32:10] <ada_ru> (I_vlxy_I) судя по всему, реально двигло сайта красит.
[18:33:54] <ada_ru> (Eugene)  отвечает (I_vlxy_I) на <судя по всему, реаль…>
а тут криво раскрасило: https://www.ada-ru.org/files/bot/2019-01-29-x3.jpg
[18:34:29] <ada_ru> (I_vlxy_I) а оно где-то сломалось. в какой-то точке, и дальше уже понеслась как есть.
[18:37:45] <ada_ru> (FROL256) это на sublime похоже
[18:38:20] <ada_ru> (I_vlxy_I) но это сайт 😊
[18:38:38] <ada_ru> (FROL256) хм.
[18:38:40] <ada_ru> (I_vlxy_I) на самом деле - это просто цветовая схема такая. она для чего угодно есть
[18:38:46] <ada_ru> (I_vlxy_I) хоть для вима
[18:38:58] <ada_ru> (FROL256) понятно
[18:56:44] <ada_ru> (Eugene)  отвечает (Максим) на <Народ сюда про Аду п…>
а вот кстати SPARK — его компилятор на чём написан? на SPARK?
[18:56:59] <ada_ru> (I_vlxy_I) камло вроде
[18:58:16] <ada_ru> (Eugene) https://github.com/AdaCore/spark2014
6. Building SPARK

ocaml compiler
[19:01:29] <ada_ru> (Максим) SPARK это не компилятор, вроде
[19:01:38] <ada_ru> (I_vlxy_I) верификатор?
[19:01:40] <ada_ru> (Максим) это средство доказательства.
[19:01:42] <ada_ru> (Максим) да
[19:01:53] <ada_ru> (Максим) а компилируется обычным GNAT-ом
[19:02:15] <ada_ru> (Максим) с выключенными проверками. мне так кажется
[19:02:30] <ada_ru> (Eugene) но это было раньше, когда весь SPARK прятался в комментариях, щас же это полноценный самостоятельный язык
[19:03:11] <ada_ru> (Максим) это подмножество Ады, значит и компилятор Ады его соберёт
[19:03:22] <ada_ru> (Eugene) расширение подмножества ады
[19:03:48] <ada_ru> (Максим) GNAT просто будет игнорировать аспекты SPARK
[19:04:16] <ada_ru> (I_vlxy_I) да, Ада же теперь расширяется с учетом существования SPARK'a
[20:01:49] <ada_ru> (nitrocerber) Спаркофагия - наше всё. А вот с ccg и формальность что? Исходники на аде формально доказаны, транслируется в си безопасным образом... Что получается? Я прост нифига не смыслю в этом всём
[20:35:52] <ada_ru> (I_vlxy_I) спаркофилия
[20:41:43] <ada_ru> (Eugene)  отвечает (nitrocerber) на <Спаркофагия - наше в…>
а далее надо полученные сишные промежуточные файлы компилировать верифицированным компилятором CompCert...