LINUX.ORG.RU

где можно применить на практике всю мощь dependent types?

 , ,


1

3

Большинство программ, с которыми я сталкиваюсь, занимаются простой и нудной работой с ОС, железом и другим софтом и не нуждается в строгой верификации кода (и даже в строгой типизации ЯП). Интересно, существуют ли задачи, в которых необходимость формальной верификации существенна из тех, к которым есть доступ обычного программиста, а не работника научных организаций. Необходимо чтоб у задачи было четкое условие, метод решения был точным (непонятно как доказывать свойства рандомизированных решений) и по возможности длинным в реализации, чтобы была большая вероятность понаделать труднообраружимых ошибок.

Пока что придумалось только 2 направления: компиляторы/оптимизаторы и решатели математических задач. Какие у кого есть соображения по этому поводу?

★★★★

Ответ на: комментарий от q0tw4

Толстовато.

Что именно?

Вот это:

занимаются простой и нудной работой с ОС, железом и другим софтом и не нуждается в строгой верификации кода (и даже в строгой типизации ЯП)

tailgunner ★★★★★ ()
Ответ на: комментарий от q0tw4

Причем тут «ты сталкиваешься»... после фразы «не нуждается [...] даже в строгой типизации ЯП» ты отправляешься либо в школу, либо на липосакцию.

tailgunner ★★★★★ ()
Ответ на: комментарий от tailgunner

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

q0tw4 ★★★★ ()
Ответ на: комментарий от q0tw4

Если внимательно писать всякие там pdf-ридеры на динамически типизированном языке и тестами обильно покрывать, то эффект будет не хуже

(зевая) Ага, ага. Много написал? Как проверял?

И кстати, посмотри в вики, что такое «строгая типизация».

tailgunner ★★★★★ ()
Ответ на: комментарий от tailgunner

Не, ну можно всё на агде переписать. Вот только мотивации нету.

q0tw4 ★★★★ ()
Ответ на: комментарий от tailgunner

И кстати, посмотри в вики, что такое «строгая типизация».

Виноват, статическая

q0tw4 ★★★★ ()
Ответ на: комментарий от tailgunner

Ладно уж с прогами, вопрос не о том. Вопрос звучит так: чего бы пописать на агде

q0tw4 ★★★★ ()
Ответ на: комментарий от q0tw4

Короче, тебе (лично тебе) от любой статической типизации толку не будет.

tailgunner ★★★★★ ()
Ответ на: комментарий от tailgunner

Наверно недаром мне руби нравится. Но всёже. Такая мощная пушка, а я её не юзаю. Непорядок.

q0tw4 ★★★★ ()
Ответ на: комментарий от q0tw4

Такая мощная пушка, а я её не юзаю.

Что толку от «мощной пушки», если артилерист (ты) - школьник?

anonymous ()
Ответ на: комментарий от q0tw4

на динамически типизированном языке и тестами обильно покрывать

зачем покрывать тестами, если по большей части это можно решить статической типизацией?

anonymous ()
Ответ на: комментарий от anonymous

Вот прикол: я не школьник, а работник программист)

q0tw4 ★★★★ ()
Ответ на: комментарий от anonymous

зачем покрывать тестами, если по большей части это можно решить статической типизацией?

А как же задача выхода за пределы массива, и так далее. Помоему даже от динамик кастов зачастую нельзя избавится без потери элегантности кода. Клёво конечно, что нельзя попутать имя переменной, но объяснять компилятору что там по логике всегда лежит объект такогото типа иногда утомительно, если компелятор не понимает полноценных вычислений на уровне типов с зависимостями от рантайма.

q0tw4 ★★★★ ()
Ответ на: комментарий от q0tw4

я не школьник, а работник программист)

Да лааадно!

anonymous ()
Ответ на: комментарий от anonymous

Ну твоё право не верить. Мне то всеравно. Я то завтра опять побреду на работу :(

q0tw4 ★★★★ ()
Ответ на: комментарий от q0tw4

Я то завтра опять побреду на работу :(

метлу не забудь

anonymous ()
Ответ на: комментарий от q0tw4

Кодер я. Гавнокодер

Ну так расти над собой. Бери Agda и думай «как бы мне применить ее к моим задачам». А пока ты думаешь «да нафиг мне Агда, у меня и без того всё нормально».

tailgunner ★★★★★ ()
Ответ на: комментарий от tailgunner

Никак не применить. Плюсы у нас. Готовая система. Переписать нереально.

q0tw4 ★★★★ ()
Ответ на: комментарий от q0tw4

Плюсы у нас. Готовая система. Переписать нереально.

А кто-то говорил о переписывании?

tailgunner ★★★★★ ()
Ответ на: комментарий от tailgunner

Ну сейчас нету еще вменяемых систем доказательства правильности написанных прог. Даже те что есть - им еще теоремы надо скормить. Встроить теоремы в код где костыль костылём погоняет сложнее переписывания. Системы с автоматическим выдумыванием теорем - пока что только моя фантазия. Так что мне нужна новая задача. Та которая раскроет весь потенциал сабжа.

q0tw4 ★★★★ ()
Ответ на: комментарий от q0tw4

Переписать нереально

тебе не нужно её переписывать. тебе нужно построить её модель и проверить корректность

jtootf ★★★★★ ()
Ответ на: комментарий от jtootf

void* на каждом шагу. Огромная куча файлов до 5 тыщ строк размером. Куча хреновых самописных контейнеров и прочих либ, часть успели перевести на буст. Чего только стоит класс с названием GuiDbArray - и контейнер, и с базой работает и гуй отображает. И работает он на старом гуи движке. Я занимаюсь новым движком который обвертка над старым. Ужос. Построение модели сложнее переписывания без костылей.

q0tw4 ★★★★ ()
Ответ на: комментарий от q0tw4

Построение модели сложнее переписывания без костылей

никакие зависимые типы не помогут тебе работать с системой, которой ты сам не понимаешь

jtootf ★★★★★ ()
Ответ на: комментарий от jtootf

Так я и не предлагаю работать с той системой. Я хочу найти себе другую задачу, ибо работу свою я «похоронил».

q0tw4 ★★★★ ()
Ответ на: комментарий от q0tw4

Я хочу найти себе другую задачу

тогда зачем комментируешь, ссылаясь на эту? возьми любую RT-задачу - поменьше производительности, побольше надёжности - и вперёд

jtootf ★★★★★ ()

Насколько понял пространную фразу топика, речь идёт о контрактном программировании. Дык применять его можно практически везде - хватило бы нервов :)

MKuznetsov ★★★★★ ()
Ответ на: комментарий от jtootf

тогда зачем комментируешь, ссылаясь на эту?

Меня просто с темы сбил пост:

Бери Agda и думай «как бы мне применить ее к моим задачам»

Но я уже «исправился» и вернулся к оригинальной теме (прошу прощения у автора вышеуказанного поста за превратное толкование его мотивов)

возьми любую RT-задачу

Станков и роботов нету в наличии. Всё, что я могу придумать полезного для собственного использования, надёжности не требует. Разве что изучить финансы и купить подключение к бирже.

q0tw4 ★★★★ ()

Нигде. В промышленной автоматизиции, в том числе в авиации, рулят тесты.

anonymous ()
Ответ на: комментарий от anonymous

Нигде. В промышленной автоматизиции, в том числе в авиации, рулят тесты.

[trolling] Это потому что там нет меня. Вот пришёл бы, сделал бы огромную безошибочную прогу с перового раза и выгнали бы тестописателей. [/trolling]

q0tw4 ★★★★ ()
Ответ на: комментарий от q0tw4

Это потому что там нет меня. Вот пришёл бы, сделал бы огромную безошибочную прогу с перового раза и выгнали бы тестописателей.

Так уже так, похоже, и сделали: заметил, как наши самолеты часто падают? :(

Boba_Fett ()
Ответ на: комментарий от q0tw4

А как ты убедишься в отсутствии ошибок в спецификации? Никак. Так что только тесты, причем не дебильные unit-тесты, а полноценные integration tests, во всех режимах работы программно-аппаратного комплекса. Кстати, в спецификации железа и взаимодействия софта и железа зависимые типы тоже никак не помогут.

anonymous ()
Ответ на: комментарий от anonymous

В некоторых задачах спецификация на порядок короче алгоритма и её проверить несложно просто просмотрев галзами. Вот такую задачу я и ищу

q0tw4 ★★★★ ()
Ответ на: комментарий от q0tw4

Есть такие задачи. Факториал, числа Фибоначчи посчитать, и тому подобная фигня.

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

anonymous ()
Ответ на: комментарий от anonymous

Это не все реальные задачи, а только те которые мы обычно юзаем придя домой после работы. Вот тест на простоту числа - математическая задача, но она на практике юзается в криптографии. Оптимизирующие компиляторы тоже сложнее модели языка который они компилируют. У кого еще есть примеры?

q0tw4 ★★★★ ()

На практике сталкивался при написании примитивов IPC. В одной из реализаций RCU ядра 2 года не могли найти ошибку, а потом обнаружили формальной верификацией. Вещи относительно простые, но параллельность дает много неочевидных багов, и все это порой сложно уместить в голове.

Pavval ★★★★★ ()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.