http://github.com/larrytheliquid/Lemmachine

шо це таке? если честно, сам не сильно понимаю , но:

(перевод я не осилил, вы уж извините )

Lemmachine is a REST'ful web framework that makes it easy to get HTTP right by exposing users to overridable hooks with sane defaults. The main architecture is a copy of Erlang-based Webmachine, which is currently the best documentation reference (for hooks & general design).

Lemmachine stands out from the dynamically typed Webmachine by being written in dependently typed Agda. The goal of the project is to show the advantages gained from compositional testing by taking advantage of proofs being inherently compositional. See proofs for examples of universally quantified proofs (tests over all possible input values) written against the default resource, which does not override any hooks.

When a user implements their own resource, they can write simple lemmas ("unit tests") against the resource's hooks, but then literally reuse those lemmas to write more complex proofs ("integration tests"). For examples see some reuse of lemmas in proofs.

The big goal is to show that in service oriented architectures, proofs of individual middlewares can themselves be reused to write cross-service proofs (even higher level "integration tests") for a consumer application that mounts those middlewares.

не уверен, что в нужный форум, но где ж еще поймут Agda, compositional tests, dependent types и прочие «доказательства» и «леммы»?

А навіщо це Вам, якщо Ви не знаєте що це таке? :^)

Disclaimer: Я в этой теме не спец, но...

Без формального доказательства приходится писать кучу юнит-тестов и надеяться, что они покрыли все случаи. А все случаи реально покрыть только в маленьких системах.
Думаю они хотят продемонстрировать возможность формального доказательства, что не только отдельные компонентны делают то, что нужно, но и вся эта service-oriented куча, несмотря на свою монстрозность, делает именно то, что нужно.

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

M>http://github.com/larrytheliquid/Lemmachine

M>шо це таке? если честно, сам не сильно понимаю

Конкурент ur/Graftid? (сам тоже не сильно понимаю )

M>>http://github.com/larrytheliquid/Lemmachine

M>>шо це таке? если честно, сам не сильно понимаю

К>Конкурент ur/Graftid? (сам тоже не сильно понимаю )

не, насколько я понял, в ur/Graftid не ставится задача доказать правильность получающейся системы

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

M>>>http://github.com/larrytheliquid/Lemmachine

M>>>шо це таке? если честно, сам не сильно понимаю

К>>Конкурент ur/Graftid? (сам тоже не сильно понимаю )

M>не, насколько я понял, в ur/Graftid не ставится задача доказать правильность получающейся системы

ну потому как она правильной будет по построению типа:

The signature of the standard library is such that well-typed Ur/Web programs "don't go wrong" in a very broad sense.