G>Я собсно как-раз работаю над такой штуковиной для доказательного программирования, которая радикально отличается в этом плане, не то язык, не то фреймворк.
G>Древовидная структура с предикатами, юзер выбирает из списка возможных следствий. Некоторые следствия создают разветвления.
А где гарантия что юзер не перепутает предикат, как он это может сделать в текстовом if ?
Доказательство какое то может быть если два программиста пишут один код на разных ЯП, а потом хитрый компилятор собирает их оба и сверяет AST или типа того. А лучше три программиста на трех разных ЯП