не, "ультраверифицировную" не получится. Придётся защищаться от фотонов, которые РОЗРУШАЮТ, и которые могут вызвать неверное выполнение инструкции процессора либо кривой доступ к памяти. Извени, я таким не займусь. У меня более простые потребности: оградить себя же самого от тупых ошибок, да так, чтобы я не особо включал моск, когда пишу код.
в простых случаях статическая типизация полезна. в сложных — зависимые типы нужны. про "синтаксическую корректность" — ээ. Статическая типизация работает после того, как с синтаксисом разобрались.
теперь понял. Корректность начинается с малого. Во многих случаях можно гарантировать корректность на основании простых типизированных лямбд, без зависимостей типов от значений (но я не про "просто-типизированное лямбда-исчисление" = "STLC"). Вот, в таких случаях корректность часто бывает просто очевидной, тот же rewriting помогает. (в coq, например, часто проще реализовать функцию с простыми типами, а затем использовать её для реализации функции с зависимыми типами, в том числе, с доказательствами про её входы-выходы. И тут "простые" типы таки хороши.)
34 comments
recommend
bookmark
subscribe
да уже было. (у меня.)
Щас набижит пукиш и скажет, чтобы ты съябывал из math.
ну ты вроде coq НА ПРАКТИКЕ петушил, не?
вот что он недавно отжоп → <epta> Говнашкель для ебанутых бомжей
Для меня.
так пишу на coq ОПЕРДЕНЬ. Ну, почти. Тем не менее, хуёвый учоный, и хуйня из-под меня (на текущий момент).
ну понятно, я опять не туда [ответил].
хочешь ультраверифицировную систему заебашить? гуд. а если БД упадет? надо БД тоже на coq. и ОСь. нутыпонел.
не, "ультраверифицировную" не получится. Придётся защищаться от фотонов, которые РОЗРУШАЮТ, и которые могут вызвать неверное выполнение инструкции процессора либо кривой доступ к памяти. Извени, я таким не займусь. У меня более простые потребности: оградить себя же самого от тупых ошибок, да так, чтобы я не особо включал моск, когда пишу код.
Верифицируй фотоны на coq, не мужик шоле.
ок. это потом в окамл экспортишь? окамл от таких ошибок не защитит, верно?
ок :[
вот вы смеетесь, а между прочем есть quantum lisp
часть — в окамл, часть — в другие языки. Конечно, я рассчитываю на их корректность. (о, кажется, мы подобное обсуждали..)
я вот что думаю. стат. типизация сама по себе нинужна. нужны зависимые типы, которые могут гарантировать логическую корректность, а не синтаксическую.
в простых случаях статическая типизация полезна.
в сложных — зависимые типы нужны.
про "синтаксическую корректность" — ээ. Статическая типизация работает после того, как с синтаксисом разобрались.
нутыпонел. ну я кривовато выразился.
не очень. п. 1 и 2 — считаю, что верны. Про "синтаксическую корректность" не понял, это вероятно.
я имел в виду корректность типов аргументов у функции.
теперь понял.
Корректность начинается с малого. Во многих случаях можно гарантировать корректность на основании простых типизированных лямбд, без зависимостей типов от значений (но я не про "просто-типизированное лямбда-исчисление" = "STLC"). Вот, в таких случаях корректность часто бывает просто очевидной, тот же rewriting помогает. (в coq, например, часто проще реализовать функцию с простыми типами, а затем использовать её для реализации функции с зависимыми типами, в том числе, с доказательствами про её входы-выходы. И тут "простые" типы таки хороши.)
это хуйня; вон на перле временно-ква[зи]кваверсальную виртуальную наноVM написали: http://yow.eventer.com/yow-2011-1004/tem...
двачаю этот толк
дома воннаби, на работе воннаби, типикал пстащебыдло
комент успешного (не-воннаби) наркомана
спасяб)
А САМ-ТО ЧЕГО ДОБИЛСЯ?
успешный блогер, ставлю на место лошков в интернете // за деньги
ну покажи хотя бы два примера
а, лень
бля, ну срсли
типа ты сам не видел
больше видел твоих бабахов, лалка
ну само собой их больше! я один, а мудаков много
двачь