Телеграмм чат группы cpprussia страница 1815

20:41пожаловаться #1

G

magras

Я бы еще не отказался послушать о приемах и концепциях из других языков. Не все можно переложить на С++, но это расширяет кругозор и иногда все равно положительно влияет на плюсовый код. Классический пример - это функциональные языки. Еще пара примеров, которые я могу сходу назвать: горутины и каналы из go, borrow checker из rust.

Рассказ о языках облегчающих формальные доказательства свойств программ тоже было бы интересно послушать. Как работает prolog? Как в erlang'е устроен рантайм что позволяет автоматически перезапускать упавший кусок вычислений? Я думаю у любого программиста есть свой список подобных вопросов на которые он хотел бы знать ответы, но "руки еще не дошли".

есть языки, специально разработанные для формальных доказательств (Haskell, но не только), но в целом вы найдете интересные «model checking» и theorem provers / proof helpers, они для этого предназначены

21:25пожаловаться #2

G

TLA+, Coq, HOL (ML), и вообще есть несколько действительно отличных научных статей по теме, написанных Zohar Manna, Amir Pnueli, и другими.
Мне было бы интересно узнать, есть ли в российских университетах активные исследования по этой теме. В конце концов, одним из первых конкретных приложений проверки моделей была правильность попыток освоения космоса, которые часто могут привести к миллионам и миллионам долларов и серьезному ущербу.

21:25пожаловаться #3

G

Также в определенной степени быстро растет область "static code analyzers". Несколько итальянских исследователей активно занимались этой темой, один из них создал компанию, которая позже была продана FB.

21:25пожаловаться #4

G

https://engineering.fb.com/2019/02/08/developer-tools/infer-team-award/

Facebook Engineering

Infer team wins Most Influential POPL Paper Award - Facebook Engineering

Infer engineers Cristiano Calcagno, Dino Distefano, and Peter W. O’Hearn, and Hongseok Yang of KAIST win ACM SIGPLAN Most Influential POPL Paper Award.

21:26пожаловаться #5

G

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

21:27пожаловаться #6

G

magras

Продолжая эту логику: перекладывание json не программирование, только чистые алгоритмы и математика могут считаться программированием.

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

21:27пожаловаться #7

G

Что касается программного обеспечения, стоит отметить, что даже на «простых» языках (C, etc) вы можете писать правильные программы, правильность которых может быть даже математически доказана -- Например микроядро seL4.
Я знал лет назад итальянского ученого (он получил высшее образование в Милане около 20-30 лет назад), который проводил исследования в этой лаборатории в Австралии вместе с Gernot Heiser.
В этой лаборатории они использовали различные инструменты для формальной проверки kernel как «математически правильного» и практически bug-free, а в последнее время они начали использовать собственные инструменты разработчика для дальнейшей специализации своей работы.

21:40пожаловаться #8

G

https://sel4.systems/Info/FAQ/proof.pml

sel4.systems

What is Proved and What is Assumed | seL4

21:41пожаловаться #9

G

Насколько мне известно, это единственная formally verified операционная система

21:41пожаловаться #10

G

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

21:41пожаловаться #11

ES

magras

Я бы еще не отказался послушать о приемах и концепциях из других языков. Не все можно переложить на С++, но это расширяет кругозор и иногда все равно положительно влияет на плюсовый код. Классический пример - это функциональные языки. Еще пара примеров, которые я могу сходу назвать: горутины и каналы из go, borrow checker из rust.

Рассказ о языках облегчающих формальные доказательства свойств программ тоже было бы интересно послушать. Как работает prolog? Как в erlang'е устроен рантайм что позволяет автоматически перезапускать упавший кусок вычислений? Я думаю у любого программиста есть свой список подобных вопросов на которые он хотел бы знать ответы, но "руки еще не дошли".

Если кратко: Prolog работает хитрым перебором, Erlang просто требует писать программы в определённом стиле с акторами ("процессы") и тогда перезапускаются только процессы. Перезапустить кусок процесса, насколько я знаю, нельзя

Alexey Veselovsky in Конференция C++ Russia

21:42пожаловаться #12

AV

Если кратко: Prolog работает хитрым перебором, Erlang просто требует писать программы в определённом стиле с акторами ("процессы") и тогда перезапускаются только процессы. Перезапустить кусок процесса, насколько я знаю, нельзя

Что такое «кусок процесса»?

21:45пожаловаться #13

ES

JetBrains Research: uniting scientists at the cutting edge

Gabriele

TLA+, Coq, HOL (ML), и вообще есть несколько действительно отличных научных статей по теме, написанных Zohar Manna, Amir Pnueli, и другими.
Мне было бы интересно узнать, есть ли в российских университетах активные исследования по этой теме. В конце концов, одним из первых конкретных приложений проверки моделей была правильность попыток освоения космоса, которые часто могут привести к миллионам и миллионам долларов и серьезному ущербу.

Да в одном JetBrains Research довольно много:
https://research.jetbrains.org/ru-ru/groups/plt_lab/
https://research.jetbrains.org/ru-ru/groups/vorpal/
https://research.jetbrains.org/ru-ru/groups/group-for-dependent-types-and-hott/

Например, у меня однокурсник в одной из групп там работает, бакалаврский диплом защищал по теме: https://habr.com/ru/company/hsespb/blog/441114/

Лаборатория языковых инструментов - исследовательская группа JetBrains Research

Лаборатория языковых инструментов - история, область интересов и основные проекты исследовательской группы JetBrain Research

21:45пожаловаться #14

G

JetBrains Research: uniting scientists at the cutting edge

Да в одном JetBrains Research довольно много:
https://research.jetbrains.org/ru-ru/groups/plt_lab/
https://research.jetbrains.org/ru-ru/groups/vorpal/
https://research.jetbrains.org/ru-ru/groups/group-for-dependent-types-and-hott/

Например, у меня однокурсник в одной из групп там работает, бакалаврский диплом защищал по теме: https://habr.com/ru/company/hsespb/blog/441114/

Лаборатория языковых инструментов - исследовательская группа JetBrains Research

Лаборатория языковых инструментов - история, область интересов и основные проекты исследовательской группы JetBrain Research

спасибо, очень интересно

21:46пожаловаться #15

ES

Pointers Are Complicated II, or: We need better language specs

Gabriele

Что касается программного обеспечения, стоит отметить, что даже на «простых» языках (C, etc) вы можете писать правильные программы, правильность которых может быть даже математически доказана -- Например микроядро seL4.
Я знал лет назад итальянского ученого (он получил высшее образование в Милане около 20-30 лет назад), который проводил исследования в этой лаборатории в Австралии вместе с Gernot Heiser.
В этой лаборатории они использовали различные инструменты для формальной проверки kernel как «математически правильного» и практически bug-free, а в последнее время они начали использовать собственные инструменты разработчика для дальнейшей специализации своей работы.

На фразе "простой Си" мне вспомнилась прекрасная https://www.ralfj.de/blog/2020/12/14/provenance.html

www.ralfj.de

Some time ago, I wrote a blog post about how there’s more to a pointer than meets the eye. One key point I was trying to make is that just because two pointers point to the same address...

21:46пожаловаться #16

ES

Alexey Veselovsky

Что такое «кусок процесса»?

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

21:47пожаловаться #17

G

Pointers Are Complicated II, or: We need better language specs

На фразе "простой Си" мне вспомнилась прекрасная https://www.ralfj.de/blog/2020/12/14/provenance.html

www.ralfj.de

Some time ago, I wrote a blog post about how there’s more to a pointer than meets the eye. One key point I was trying to make is that just because two pointers point to the same address...

собственно, поэтому я заключил "простой" в кавычки

21:47пожаловаться #18

G

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

21:47пожаловаться #19

G

Pointers Are Complicated II, or: We need better language specs

На фразе "простой Си" мне вспомнилась прекрасная https://www.ralfj.de/blog/2020/12/14/provenance.html

www.ralfj.de

Some time ago, I wrote a blog post about how there’s more to a pointer than meets the eye. One key point I was trying to make is that just because two pointers point to the same address...

это, кстати, одна из причин, почему современный C++ стимулирует использование стандартной библиотеки, так что эти подверженные ошибкам детали абстрагируются std containers и другими facilities, если вам действительно, действительно не нужно возиться с этими техническими аспектами (для определенных программ)