October 30th, 2017

Book

Contracts first

Тут из альтернативной вселенной сообщают, что завтипы говно и не нужны.

Вместо этого берете язык с простыми типами и контрактами в стиле Eiffel https://www.eiffel.com/values/design-by-contract/introduction/ и скармливаете статик ассерты в http://why3.lri.fr/#users которая дальше их скармливает пруверам из списка http://why3.lri.fr/#provers

Оно и в кок конечно умеет скармливать, но пруверы для конечных теорий (типа SMT FixedSizeBitVectors) по понятным причинам и работают лучше, и точнее моделируют машинное представление.
Book

Клон N2O.hs

http://hackage.haskell.org/package/threepenny-gui

Идея та же - вебсокет-сервер с RPC в обратную сторону, т.е. из х-я в б-р.

Причем даже через eval:

https://github.com/HeinrichApfelmus/threepenny-gui/blob/master/js/ffi.js#L78

Оно там на говне и палках, но можно понадергать идей и кода и постепенно унифицировать.