Посмотрел наконец повнимательнее на продукт сумрачного W3C-шного гения - WebAssembly ( Read more... )

Есть еще одно забавное поделие - язычок ivory - safe язычок С-образного типа (у которого естественно есть интегратор под названием tower). Затея сама по себе пример ленивого языкового дизайна - и потому что на haskell и потому что действительно ленивого ( Read more... )

По поводу:
https://kouzdra.livejournal.com/4404809.html
https://kouzdra.livejournal.com/4410328.html

были демоны была бага - вчера вечером засабмитил - пофиксили (говорят - я пока не проверял).

Upd: проверил и правда пофиксили

Пара слов по тому примеруПосле того как стало понятно, что основа совинной методы - агрессивное разворачивание кода, в общем-то стало понятно и "как оно это доказывает":
( Read more... )

В общем - разобрался я "что это было и как это называется" (© Леонид Соболев). На деле оказалось не просто "тупо и просто", а "очень тупо и просто" - и довольно коряво, но для своего реального назначения вероятно самое то ( Read more... )

Разобрался с примерчиком про деление. Вкратце - как и ожидалось, просто ошибка в генерации промежуточного кода из-за которой не сходятся типы:
( Read more... )

Одна из причин моего к нему интереса - именно что "вроде бы на этом можно писать" (потому что на WhyML писать невозможно - да собственно и не предполагалось - его делали для опытов с доказательством всяких достаточно навороченных алгоритмов).

Так-то там ничего особенно принципиально нового нет.

Вообще я конечно хренею тихо от мифа о "динамично развивающейся отрасли IT":

Ну вот то что я по dafny и saw пишу - это вообще-то говоря логика Хоара доведенная наконец до практически юзабельного вида ( Read more... )

(причина дафнячества простая - мне с этим и около надо разобраться более или менее подробно - потому разбираюсь - ну и что-то пощу - отчасти "для памяти", отчасти "для публики" и в видах народного просвещения).Из того же примера: захотелось посмотреть как решаются проблемы с алиасингом - ну соответственно инкремент массива выделился в функцию "о ( Read more... )

Раз уж пошло такое - иллюстрация к этому: https://kouzdra.livejournal.com/4407243.htmlВот такой код компилируется и работает:

var lo, hi := 2, 4;
var a := new int[6];
forall i | 0 <= i < a.Length {
a [i] := (i + 1) * 10;
}
ghost var prevElements := a[..];
var i := 0;
while i < a.Length
( Read more... )