Coq 8.5

А где скриншоты?

Да и предикативный вывод лем так и не починили :(

формального описания семантики для Си тупо не существует

Втопку этот недоязык. Есть же раст, давайте напишем для него (и будем тогда уже писать всю системщину на нем). Заодно докажем или опровергнем ту надежность, которую нам обещают его автора. Или для реальной многопоточнсти/многопроцессорности с одновременным доступом к памяти и недетерминированной перестановкой порядка выполнения команд еще не придумали формализма?

Либо мягкое «жь» (в русском отсутствует) в аргентинском испанском.

Есть же раст, давайте напишем для него

Для раста формальная семантика пока не написана. На сегодняшний день у них даже синтаксиса формального нет.

http://plv.mpi-sws.org/rustbelt/

На сегодняшний день у них даже синтаксиса формального нет.

Как-то нехорошо получилось без пруфов. Вот: https://doc.rust-lang.org/grammar.html , искать по слову «FIXME»

Ох, какая интересная штучка.

Вот бы освоить, а то все пердолю скалку для скучных дядей. А так было бы чем выдрюкиватсья.

Un coq s'est mis a faire des cocoricos au lieu d'Aurore

Нам очень интересно, информируй нас дальше.

На сегодняшний день у них даже синтаксиса формального нет.

У языка даже спецификации нет:

Rust does not have an exact specification yet

Как вообще так можно было выпускать версию 1.0?.. Не то что Go. Спецификация есть и по сравнению с С++ (1300+ страниц) и Джавой очень компактная. Интересно, как по сравнению с Си?

Не плачь, все уже исправили. Не нужно виртуальных машин, написаных на убогих плюсах. Есть JVM на Java: https://en.wikipedia.org/wiki/Jikes_RVM

Не неси ересь. Единственная истинная джава-машина находится у преподобного Гослинга. Она сделана из чистого золота и внешне похожа на кофе-машину.

Все остальные джава-машины суть косорукие реплики с этого богородичного образа.

А по теме опять глупость. Верифицировать сишечку невозможно, ибо нет в ней искры. Это просто еще один антивирус касперский для программ, бессмысленный и беспощадный! А верифицировать джаву можно только для той единственной джава-машины. Это полезно, конечно, но не слишком функционально.

А по теме опять глупость. Верифицировать сишечку невозможно

Ты тупенький, или просто охуевший? Какая такая сраная сишечка? Там божественную Джаву верифицируют.

Очень даже сделает. Огромное количество ошибок программисты делают из за того, что gcc не переваривает корректный код и поэтому приходится писать некорректный.

Твоя клоудана поначалу была забавной, но её тут стало слишком много. Найди себе другой топик, а в этом обороты своей шизофазии поумерь.

Потому что Coq разработали французы.

В каждой шутке есть доля шутки.

Невозможность реализовать алгоритм прямо влечет за собой костыли и этого не изменить.

Там верифицируют и то и другое. И оба раза безумный фейл, потому что сишечка слишком убога и непредсказуема для верификации, а джава слишком божественна и поэтому непознаваема для сирых...

Думаю, что джаву и си, да и вообще любой ЯП принципиально несложно описать формально так, чтоб любая доказанная теорема о некоторой программе 100% выполнялась на практике (ну если не принимать во внимание долгие вычисления, которые юзер сочтет зависанием). Проблема в том, что для всех более менее сложных реально работающих программ, не то что доказывать теоремы, формулировать их потребуеться очень долго. Да и 100% сорвется доказательство, так как прогамма всегда содержит баги, хотя бы те, которые воспроизводятся только на практически бесполезных юзкейсах и никак не мешают нормальной работе программы (разве что могут быть использованы хакерами). Можно конечно сразу при написании проверять, но всеравно времязатраты будут нереальными, проще взять тот же rust для базовой защиты и не забывать про тесты.

Сущая ахинея. Процедурные языки в принципе не вертфицируются в силу свой убогой природы. Функциональные же нефункциональны. И только джава явила собой сплав процедурности помноденной на императив объектной парадигмы «все уже сделано» в чем её уникальность и состоит .

Ололошки, да ты реально ебанутый...

Джава хороша только одним: мизерное количество возможностей, следовательно очень легко построить мат модель (ну если только не многопоточную, там у джавы та же мутексная попа, что и везде). В си же придется в модели учитывать например то что если у нас есть struct { int x; int y; } s, то &s.x + 1 == &s.y и тому подобное, что в принципе муторно, зависит от компилятора итп, но вполне выполнимо.

Корректность доказывается тестами.

Докажи тестами, что a + b > a для всех положительных целых a и b. После тепловой смерти Вселенной возвращайся, обсудим, в чем ты был неправ.

Для верификации Си и вообще чего угодно императивного не надо строить модель семантики Си. Достаточно построить модель минимальной тупейшей виртуальной машины, и дальше тупо Хоаровскую логику применять (ну или ее расширение - separation logic, как в compcert). Отдельно доказывается корректность перевода твоего убогого Си или божественного Джава-кода в эту машину, но это уже задача совсем тривиальная.

Хотел пример привести, но он зараза не работает. Но суть всеравно понятна.

#include <stdio.h>
#include <memory.h>
#include <stdlib.h>

const char* text = "Hello world\n";

void f() {
  printf(text);
}

void g() {}

typedef void (*fun)();

int main() {
  char* code = malloc((char*)(&g)-(char*)(&f));
  memcpy(code, &f, (char*)(&g)-(char*)(&f));
  ((fun)code)();
  return 0;
}

Поидее это хеловорлд. Интересно как подобное будет выглядеть в виртуальной машине? То, что тут его можно легко заменить на f(); не значит, что так будет всегда. А если усложнить задачу и написать содержимое code сразу в виде литерала? Да, конечно переносимости уже не будет, но доказывать хотя б для конекретной машины надо же.

новый движок тактик;

Спасибо, наконец то смог в танчиках нагнуть рандом

Ок, доказывай хоть для x86, разницы никакой. Формальных Хоаровских моделей x86 хоть жопой жуй.

Да я что, просто в идеале надо завязаться именно на модель x86 со всеми ее прибамбасами + низкоуровневые либы в виде отдельных моделей (ну или автогенерация теорем о libc по результатам анализа ее и ядра). Не помешал бы уже бот - автодоказыватель, иначе просто человекочасов на доказательства не хватит. Но о простой виртуалке для Си речь не идет, только если рассмотреть урезанный Си, с запретами на всякую гадость с самоизмененеим кода и особо извращенные операции с памятью. С джавкой все проще - там и так эти ограничения стоят. Вот почему не следует ожидать строгих доказательств произвольного Си-кода в ближайшем десятилетии. Да и раст пойдет с оговоркой, что все unsafe аксиомами. Но перспектив больше на счет раста.

А еще есть это, толкько C#:

using System;
namespace project5
{
    class Program
    {
        static void Main(string[] args)
        {
         
        }

        class Petux
        {
            private int petux = "kukareku!";
            
            public Petux():this(5)
            {
                
            }

            public Petux(int i):this()
            {
                
            }
        }

    }
}

А еще есть это, толкько C#

Нее, шарп хороший. По сути шарп это то, чем должна была быть джава в идеальном мире. Жалко что народ попутал и везде поставил этот недошарп, в то время истинный шарп прозябает в роли, в которой должна была быть гавноджава. Если б я нашел работу на шарпе, я б туда с удовольствием пошел бы, а на джаву не приправленную груви, котлином или скалой смотреть противно.