Re[19]: Жизнь без IDE
От: LaPerouse  
Дата: 27.10.09 22:40
Оценка:
Здравствуйте, thesz, Вы писали:

LP>>Вим, чтобы избежать подобной судьбы, ввел два режима


T>Широта твоей неосведомлённости просто поражает.


А какова твоя версия появления двух режимов?
Социализм — это власть трудящихся и централизованная плановая экономика.
Re[16]: Жизнь без IDE
От: LaPerouse  
Дата: 27.10.09 22:43
Оценка:
Здравствуйте, thesz, Вы писали:

T>Здравствуйте, LaPerouse, Вы писали:


T>>>И это проще, чем добавление "каталог:\n\tchdir каталог\nmake all"?

T>>>В случае make у меня всё единообразно — есть список целей, есть способы их достижения. В случае Eclipse?..
LP>>Вот не понимаю я, при чем тут эклипс. nmake — утилита сборки, эклипс — среда разработки. Совершенно разные вещи. Я думал, что тебе тяжело сынтегрировать эклипс с nmake. А теперь я и не знаю, что думать

T>Сборка — это часть разработки.

T>Кстати, влияющая на многие стороны разрабатываемого проекта.

Сборка — это сборка. И к эклипсу это не имеет никакого отношения. Все. Точка. Признай наконец-то что сказал чушь.

T>Вот скажи, ты .bat файлами пользуешься?

T>Если пользуешься, они компилируются в Java байт-код?
T>Так и здесь — на Agda2 ты можешь делать ответственные вещи. Из которых получаются Java классы. Которые ты используешь в других местах твоего проекта.

Нет, спасибо. Генерят код для жабы те, кто не умеет на ней писать.
Социализм — это власть трудящихся и централизованная плановая экономика.
Re[20]: Жизнь без IDE
От: thesz Россия http://thesz.livejournal.com
Дата: 28.10.09 07:18
Оценка:
Здравствуйте, LaPerouse, Вы писали:

LP>Здравствуйте, thesz, Вы писали:


LP>>>Вим, чтобы избежать подобной судьбы, ввел два режима

T>>Широта твоей неосведомлённости просто поражает.
LP>А какова твоя версия появления двух режимов?

Это не моя, это общепринятая. От автора, так сказать. vi — последователь командных редакторов Unix, см. его историю.

Joy explained that the terse, single character commands and the ability to type ahead of the display were a result of the slow 300 baud modem he used when developing the software and that he wanted to be productive when the screen was painting slower than he could think.[6]


И, кстати, vi старше Emacs.

Так что тут ты неправ вообще нигде.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Re[17]: Жизнь без IDE
От: thesz Россия http://thesz.livejournal.com
Дата: 28.10.09 07:21
Оценка: +1
Здравствуйте, LaPerouse, Вы писали:

T>>Сборка — это часть разработки.

T>>Кстати, влияющая на многие стороны разрабатываемого проекта.
LP>Сборка — это сборка. И к эклипсу это не имеет никакого отношения. Все. Точка. Признай наконец-то что сказал чушь.

Вообще-то имеет.

Ещё раз. Сложности сборки проектов с кодогенерацией под текущими средами разработки практически полностью блокируют её использование.

T>>Вот скажи, ты .bat файлами пользуешься?

T>>Если пользуешься, они компилируются в Java байт-код?
T>>Так и здесь — на Agda2 ты можешь делать ответственные вещи. Из которых получаются Java классы. Которые ты используешь в других местах твоего проекта.
LP>Нет, спасибо. Генерят код для жабы те, кто не умеет на ней писать.

Да-да. А компиляторами из Си в ассемблер пользуются те, кто не умеет писать на ассемблере.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Re[20]: Жизнь без IDE
От: dr.Chaos Россия Украшения HandMade
Дата: 28.10.09 08:10
Оценка: +1
Здравствуйте, LaPerouse, Вы писали:

LP>А какова твоя версия появления двух режимов?


Ну начнём с того что их далеко не 2.
Побеждающий других — силен,
Побеждающий себя — Могущественен.
Лао Цзы
Re[18]: Жизнь без IDE
От: LaPerouse  
Дата: 28.10.09 08:14
Оценка: :))
Здравствуйте, thesz, Вы писали:

T>Здравствуйте, LaPerouse, Вы писали:


T>>>Сборка — это часть разработки.

T>>>Кстати, влияющая на многие стороны разрабатываемого проекта.
LP>>Сборка — это сборка. И к эклипсу это не имеет никакого отношения. Все. Точка. Признай наконец-то что сказал чушь.

T>Вообще-то имеет.


T>Ещё раз. Сложности сборки проектов с кодогенерацией под текущими средами разработки практически полностью блокируют её использование.


Это бред. Еще раз. Eclipse не имеет никакого отношения к сборке проекта. И он не осложняет сборку проекта. Вообще никак.


LP>>Нет, спасибо. Генерят код для жабы те, кто не умеет на ней писать.

T>Да-да. А компиляторами из Си в ассемблер пользуются те, кто не умеет писать на ассемблере.

передергивать-то не надо. java не ассемблер а высокоуровневый язык, сравнимый с Agda, на котором ты собрался генерировать java-код.
Социализм — это власть трудящихся и централизованная плановая экономика.
Re[19]: Жизнь без IDE
От: lomeo Россия http://lomeo.livejournal.com/
Дата: 28.10.09 09:03
Оценка:
Здравствуйте, LaPerouse, Вы писали:

LP>>>Нет, спасибо. Генерят код для жабы те, кто не умеет на ней писать.


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

T>>Да-да. А компиляторами из Си в ассемблер пользуются те, кто не умеет писать на ассемблере.

LP>передергивать-то не надо. java не ассемблер а высокоуровневый язык, сравнимый с Agda, на котором ты собрался генерировать java-код.

Посмотри на Agda. Java по сравнению с этим языком не дотягивает даже до ассемблера по сравнению с С.
Re[19]: Жизнь без IDE
От: VoidEx  
Дата: 28.10.09 11:15
Оценка: :))
Здравствуйте, LaPerouse, Вы писали:

LP>передергивать-то не надо. java не ассемблер а высокоуровневый язык, сравнимый с Agda, на котором ты собрался генерировать java-код.

Правда что ли?
Re[20]: Жизнь без IDE
От: LaPerouse  
Дата: 28.10.09 11:47
Оценка:
Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, LaPerouse, Вы писали:


LP>>>>Нет, спасибо. Генерят код для жабы те, кто не умеет на ней писать.


L>Ты это серьёзно? Неужели ты не видишь, что в java полно boilerplate кода, от которого не избавишься из-за недостатков самого языка?


Видишь ли, java — объектно-ориентированный язык, а копипастный код — одно из зол, для борьбы с которой ООП и создавался. Так что зачастую такой код появляется не благодаря, а вопреки идеям, лежащим в основе языка. Но я не собираюсь петь дифирамбы объектной ориентированности и признаю, что на практике копипастный код часто имеет место быть (и у меня тоже, хотя я делаю многое, чтобы этого избежать). Но что ты предлагаешь взамен? Почему ты думаешь, что академический язычок, рядом с которым хаскель выглядит стандартом промышленного программирования, поможет легко решить эту проблему, не породив новые?

T>>>Да-да. А компиляторами из Си в ассемблер пользуются те, кто не умеет писать на ассемблере.

LP>>передергивать-то не надо. java не ассемблер а высокоуровневый язык, сравнимый с Agda, на котором ты собрался генерировать java-код.
L>Посмотри на Agda. Java по сравнению с этим языком не дотягивает даже до ассемблера по сравнению с С.

Ну-ну. Расскажите вкратце, что оно из себя представляет. Я почитал вики и ничего не понял. Почему agda, а не epigram? И кстати, там написано, что Агда — "theorem prover". Я слабо разбираюсь во всем этом, но всегда думал, что автоматическое доказательство теорем — удел логических языков типа пролога. Ведь для формулировки теорем нужна возможность формулировать утверждения и задавать цели, которые среда будет стремиться автоматически достичь. А Agda — функциональный язык. Как так?
Социализм — это власть трудящихся и централизованная плановая экономика.
Re[21]: Жизнь без IDE
От: lomeo Россия http://lomeo.livejournal.com/
Дата: 28.10.09 12:58
Оценка:
Здравствуйте, LaPerouse, Вы писали:

LP>Видишь ли, java — объектно-ориентированный язык, а копипастный код — одно из зол, для борьбы с которой ООП и создавался. Так что зачастую такой код появляется не благодаря, а вопреки идеям, лежащим в основе языка.


Во-первых, ООП создавался не для борьбы с копипастным кодом. Во-вторых, у ООП есть ряд серьёзных недостатков, хорошо об этом написано у thesz здесь.

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


А у Явы этих недостатков ещё больше. Отсутствие функций высшего порядка приносит просто огромную кучу бойлерплейта. Декоратор для группы строк:

    public boolean startsWith(String s)
    {
        for (String str: strings) {
            if (str.startsWith(s)) {
                return true;
            }
        }

        return false;
    }

    public boolean endsWith(String s)
    {
        for (String str: strings) {
            if (str.endsWith(s)) {
                return true;
            }
        }

        return false;
    }


И ещё куча таких методов, отличающихся только выделенным. Понасоздавать на каждую функцию по классу? Это проблемы языка, а не программиста. Этот код должен генериться. Ну, или копи-пастится, да

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


Я не пользуюсь Agda в разработке. Но многие приёмы из неё успешно использую в Haskell.
На "Не породив новые" отвечу так — не попробовав не узнаешь.

LP>Ну-ну. Расскажите вкратце, что оно из себя представляет. Я почитал вики и ничего не понял.


Так не бывает. Что именно ты не понял? Dependently Typed Programming in Agda читал?

LP>Почему agda, а не epigram?


Субъективно. Мне ближе его синтаксис.

LP>И кстати, там написано, что Агда — "theorem prover". Я слабо разбираюсь во всем этом, но всегда думал, что автоматическое доказательство теорем — удел логических языков типа пролога.


Есть такая изумительная штука, называется Curry-Howard изоморфизм. Это утверждение о том, что типы данных, есть аксиомы, типы функций — есть теоремы, а программмы (тело функций) — есть доказательство этих теорем. Изоморфизм там явный, его сразу видно. Так вот, в этом смысле между доказательством теоремы и написанием программы нет никакой разницы.

Я тебе уже приводил пример автоматического вывода тела функции по её типу. Этот вывод как раз и строится по аналогии с доказательством теоремы, изоморфной типу этой функции.

LP>Ведь для формулировки теорем нужна возможность формулировать утверждения и задавать цели, которые среда будет стремиться автоматически достичь. А Agda — функциональный язык. Как так?


Curry-Howard изоморфизм. Меня в своё время очень сильно зацепило. Почитай, там и примеры есть отображения.
Re[19]: Жизнь без IDE
От: thesz Россия http://thesz.livejournal.com
Дата: 28.10.09 13:23
Оценка:
Здравствуйте, LaPerouse, Вы писали:

T>>Вообще-то имеет.

T>>Ещё раз. Сложности сборки проектов с кодогенерацией под текущими средами разработки практически полностью блокируют её использование.
LP>Это бред. Еще раз. Eclipse не имеет никакого отношения к сборке проекта. И он не осложняет сборку проекта. Вообще никак.

Осложняет. Осложняет, уверяю тебя.

Нельзя взять Eclipse и сделать в нём какой угодно проект. Надо ещё всякого другого знать и использовать.

LP>>>Нет, спасибо. Генерят код для жабы те, кто не умеет на ней писать.

T>>Да-да. А компиляторами из Си в ассемблер пользуются те, кто не умеет писать на ассемблере.
LP>передергивать-то не надо. java не ассемблер а высокоуровневый язык, сравнимый с Agda, на котором ты собрался генерировать java-код.

Любой язык программирования является сравнимым с другим. Например, автокод сравним с Прологом, PL/1 — с Java, C# с Direct3D Shading Language. Нам же интересны результаты сравнения, а не просто факт сравнимости.

Поэтому.

Mixfix синтаксис в Java есть?

Параметрический полиморфизм в Java есть?

Функции высших порядков в Java есть?

Зависимые типы данных в Java есть?

Строгое формальное доказательство соответствия программ спецификации есть?
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Re[22]: Жизнь без IDE
От: LaPerouse  
Дата: 28.10.09 13:56
Оценка:
Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, LaPerouse, Вы писали:


LP>>Видишь ли, java — объектно-ориентированный язык, а копипастный код — одно из зол, для борьбы с которой ООП и создавался. Так что зачастую такой код появляется не благодаря, а вопреки идеям, лежащим в основе языка.


L>Во-первых, ООП создавался не для борьбы с копипастным кодом.


Здесь вообще мало говорится о том, почему он появился.

L>Во-вторых, у ООП есть ряд серьёзных недостатков, хорошо об этом написано у thesz здесь.


Здесь практически ничего не написано.

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

L>А у Явы этих недостатков ещё больше. Отсутствие функций высшего порядка приносит просто огромную кучу бойлерплейта. Декоратор для группы строк:

Пиши так:

    public boolean startsWith(final String s)
    {
    return atLeastOne(new Predicate<String>() {
            public boolean predicate(String str)
            {
                return str.startsWith(s);
            }
        });
    }

    public boolean endsWith(final String s)
    {
        return atLeastOne(new Predicate<String>() {
            public boolean predicate(String str)
            {
                    return str.startsWith(s);
            }
        });
    }
    
    private boolean atLeastOne(Predicate<String> predicate)
    {
        for (String str: strings) {
            if (predicate.predicate(str)) 
            {
                return true;
            }
        }

        return false;
    }


Predicate<T> определяется один раз и его хватает очень намного
public interface Predicate <T>
{
    boolean predicate(T object);
}


L>И ещё куча таких методов, отличающихся только выделенным. Понасоздавать на каждую функцию по классу?


Да нет, использовать то, что есть. И просить у Sun сделать ФВП в 7-ой яве

L>Так не бывает. Что именно ты не понял? Dependently Typed Programming in Agda читал?


Да я ничего не понял, честное слово. Не читал.

LP>>И кстати, там написано, что Агда — "theorem prover". Я слабо разбираюсь во всем этом, но всегда думал, что автоматическое доказательство теорем — удел логических языков типа пролога.


L>Есть такая изумительная штука, называется Curry-Howard изоморфизм. Это утверждение о том, что типы данных, есть аксиомы, типы функций — есть теоремы, а программмы (тело функций) — есть доказательство этих теорем. Изоморфизм там явный, его сразу видно. Так вот, в этом смысле между доказательством теоремы и написанием программы нет никакой разницы.


Ладно, спасибо за ссылки, просто с этим надо очень серъезно разбираться. С ходу понять не получается (по крайней мере у меня).
Социализм — это власть трудящихся и централизованная плановая экономика.
Re[23]: Жизнь без IDE
От: lomeo Россия http://lomeo.livejournal.com/
Дата: 28.10.09 14:22
Оценка: 1 (1)
Здравствуйте, LaPerouse, Вы писали:

L>>Во-первых, ООП создавался не для борьбы с копипастным кодом.

LP>Здесь вообще мало говорится о том, почему он появился.

The idea occurred to them of grouping the different types of ships into different classes of objects; each class of objects being responsible for defining its own data and behavior


L>>Во-вторых, у ООП есть ряд серьёзных недостатков, хорошо об этом написано у thesz здесь.

LP>Здесь практически ничего не написано.

С наследованием, классами и ООП целиком обязательно ассоциируется, во-первых, неявная диспетчеризация по первому аргументу функции, во-вторых, группировка методов вокруг классов и, в-третьих, но не в последних по значению, открытые типы данных


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

L>>А у Явы этих недостатков ещё больше. Отсутствие функций высшего порядка приносит просто огромную кучу бойлерплейта. Декоратор для группы строк:

LP>Пиши так:


Ну, когда я первый раз на ФП посмотрел, я так и писал Только согласись, что

1. Кода меньше не стало
2. От бойдерплейта мы не избавились (заменили цикл на объявление локал класса)
3. У тебя ошибка в коде связанная с копи-пастом
4. На языках, поддерживающих ФВП первые три пункта отсутствовали бы как класс:

endsWith = any . endsWith
startsWith = any . startsWith


Ой! Тут тоже бойлерплейт! Да, но в этом языке его можно удалить:

any1 = (any .)
endsWith = any1 endsWith
startsWith = any1 startsWith


LP>Predicate<T> определяется один раз и его хватает очень намного


Да не хватает их ни фига. Я пример ещё тривиальный привёл. Для стандартных классов можно нагенерить Function2<T,A,R> и использовать. Но тут мы просто разделяем сложность. Клиенту то попроще будет, а вот библиотеку такую писать — сложнее.

Кстати, вот это, думаю, тебе будет интересно:
http://www.rsdn.ru/article/java/JavaFP.xml
Автор(ы): Евгений Кирпичев aka jkff
Дата: 28.12.2008
Официально язык Java поддерживает только объектно-ориентированную парадигму, которая не всегда позволяет сделать код компактным, легко читаемым и удобным в поддержке. Однако Java-гуру умудряются использовать имеющиеся в Java возможности для применения в Java-коде функционального стиля программирования, который в некоторых случаях позволяет радикально улучшить читаемость кода (делая его более декларативным), а также упростить его поддержку и развитие. Надеемся, что данная статья будет полезна многим Java-программистам разного уровня.
Большая часть данной статьи не имеет отношения к собственно функциональному программированию (далее – ФП). В основном будут рассмотрены способы повышения читаемости некоторых часто встречающихся паттернов, особенно при использовании функционального стиля, и без которых об ФП не может быть и речи. О приемах собственно ФП будет сказано совсем немного, ближе к концу статьи.


L>>И ещё куча таких методов, отличающихся только выделенным. Понасоздавать на каждую функцию по классу?

LP>Да нет, использовать то, что есть. И просить у Sun сделать ФВП в 7-ой яве

+1. А потом просить карринг, а потом ленивость..

L>>Так не бывает. Что именно ты не понял? Dependently Typed Programming in Agda читал?

LP>Да я ничего не понял, честное слово. Не читал.

Ну почитай, тогда вернёмся.

LP>Ладно, спасибо за ссылки, просто с этим надо очень серъезно разбираться. С ходу понять не получается (по крайней мере у меня).


Я думаю, с первого раза даже у thesz не получалось
Re[24]: Жизнь без IDE
От: thesz Россия http://thesz.livejournal.com
Дата: 28.10.09 17:04
Оценка: :)
Здравствуйте, lomeo, Вы писали:

L>Я думаю, с первого раза даже у thesz не получалось


Ха!

Полтора года ломал голову.

Да и сейчас ещё не очень силён.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Re[7]: Жизнь без IDE
От: artem_korneev США https://www.linkedin.com/in/artemkorneev/
Дата: 29.10.09 14:45
Оценка:
Здравствуйте, LaPerouse, Вы писали:

LP>По сравнению с вышеперечисленным хардкорная работа в обычном текстовом редакторе выглядит прошлым веком. Вимы и емаксы кажутся настолько архаичными, примитивными и неудобными, что заставить себя набрать в них хотя бы двадцать строчек кода уже не могу (раньше мог).


У тебя какое-то странное представление о работе в vim/emacs.
Что будем называть IDE? Если IDE это Integrated Development Environment, то в этом смысле, настроенные vim/emacs — тоже вполне себе IDE.
Автокомплит кода там есть. Правда, он не такой продвинутый, как, например, в Visual Studio, но в принципе — хватает. Особенно, если использовать CEDET (для emacs) — тогда это уже дополнение не просто по словам, а контекстно-зависимое, "умное дополнение". Хотя там ещё есть что усовершенствовать.
Некоторая интеграция с отладчиком и переход на строчки с ошибками компиляции — есть.
Переход к месту объявления функции/переменной, перечисление мест, где функция или переменная используется — всё это есть.
Некоторые ошибки — подсвечиваются во время редактирования(непарные скобки, например). Некоторые — нет. Кстати, в том же emacs есть некоторые любопытные функции, которых я пока не видел в "больших IDE" — например, принудительное форматирование блока кода. Иногда это помогает заметить логические ошибки в чужом коде. Хотя сейчас большинство IDE форматируют код при наборе, так что для новых проектов это становится неактуально.

Посему, не стоит думать что vim/emacs так уж кардинально отстают от других IDE по функциональности. В тоже время, "готовые" IDE зачастую сильно завязаны на конкретный компилятор, систему сборки и т.д. Например, в том проекте, над которым я сейчас работаю, этим летом сборку перевели на мейкфайлы. Соответственно, Visual Studio их не понимает и некорректно подсвечивает активные/неактивные участки кода.
С уважением, Artem Korneev.
Re[20]: Жизнь без IDE
От: Аноним  
Дата: 01.11.09 09:58
Оценка:
Здравствуйте, thesz, Вы писали:

T>Строгое формальное доказательство соответствия программ спецификации есть?


http://krakatoa.lri.fr/
Re[21]: Жизнь без IDE
От: deniok Россия  
Дата: 01.11.09 10:21
Оценка:
Здравствуйте, Аноним, Вы писали:

А>Здравствуйте, thesz, Вы писали:


T>>Строгое формальное доказательство соответствия программ спецификации есть?


А>http://krakatoa.lri.fr/


А для описания спецификаций учить дополнительный язык, Java Modeling Language? Который разбирается Krakatoa, который передает результат в Why, который вызывает прувер, например, COQ, чтобы проверить все спецификации?

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

Тем более, что наличие в этом JML аннотаций типа pure, подсказывает мне, что стандартный императивный джавовский дизайн всё равно менять придется.
Re[22]: Жизнь без IDE
От: Аноним  
Дата: 01.11.09 11:01
Оценка:
Здравствуйте, deniok, Вы писали:

D>Спасибо, но если от меня потребуют доказано соответствующий спецификации код, я лучше непосредственно из COQ нагенерю хаскельный код с приложенным доказательством корректности, или на Agda2 напишу.


А если, извините, требуется код на Java? Вот требуется, и всё тут? Тогда уж лучше так, чем совсем без аннотаций.

D>Тем более, что наличие в этом JML аннотаций типа pure, подсказывает мне, что стандартный императивный джавовский дизайн всё равно менять придется.


И это прекрасно.
Re[23]: Жизнь без IDE
От: deniok Россия  
Дата: 01.11.09 11:13
Оценка:
Здравствуйте, Аноним, Вы писали:

А>Здравствуйте, deniok, Вы писали:


D>>Спасибо, но если от меня потребуют доказано соответствующий спецификации код, я лучше непосредственно из COQ нагенерю хаскельный код с приложенным доказательством корректности, или на Agda2 напишу.


А> А если, извините, требуется код на Java? Вот требуется, и всё тут? Тогда уж лучше так, чем совсем без аннотаций.


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

java не ассемблер а высокоуровневый язык, сравнимый с Agda, на котором ты собрался генерировать java-код

Re[24]: Жизнь без IDE
От: Аноним  
Дата: 01.11.09 11:29
Оценка:
Здравствуйте, deniok, Вы писали:

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

D>

D> java не ассемблер а высокоуровневый язык, сравнимый с Agda, на котором ты собрался генерировать java-код



Речь выше шла о тезисе, что средств формальной верификации для Java нет. Я же говорю, что таки есть.
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.