История изменений

Какая она жуткая…

Ну, я согласен что покрасивее - поприятнее. Но это не очень важно на самом деле. Иногда бывает прям сильно покрасивее получается. Но это вопрос уже конечно некоторых дополнительных усилий - чтобы было красиво.

И в неё достаточно сложно втыкать дополнительные ограничения, которых нет в Rust, так как там нет зависимых типов. А если начинаем что-то втыкать в транслированный код, то автоматически теряем связь с изначальным.

Это не так задумано.
У нас есть исходный код на Расте. Мы транслируем его в код на кок. Это наша модель. С большой долей уверенности можно говорит что она соотвествует оригинальному коду, так как

1) это бекэнд к оригинальному компилятору раста (т.е. парсинг и построение дерева выполняет rustc)

2) транслятор транслирует 99% примеров из rust by examples (т.е. тесты есть)

Имея эту модель, нужно просто писать про неё свои утверждения непосредственно в коке. Т.е. не нужно менять код модели, нужно писать утверждения o модели.

Т.е. например если у нас есть на расте функция (прошу прощения заранее, пример не компилировал, раст больше года не видел)

fn myfun(n) -> nat { return n + 1 }

Lemma myfun_correct n : myfun n = n + 1.

Какая она жуткая…

Ну, я согласен что покрасивее - поприятнее. Но это не очень важно на самом деле. Иногда бывает прям сильно покрасивее получается. Но это вопрос уже конечно некоторых дополнительных усилий - чтобы было красиво.

И в неё достаточно сложно втыкать дополнительные ограничения, которых нет в Rust, так как там нет зависимых типов. А если начинаем что-то втыкать в транслированный код, то автоматически теряем связь с изначальным.

Это не так задумано.
У нас есть исходный код на Расте. Мы транслируем его в код на кок. Это наша модель. С большой долей уверенности можно говорит что она соотвествует оригинальному коду, так как

1) это бекэнд к оригинальному компилятору раста (т.е. парсинг и построение дерева выполняет rustc)

2) транслятор транслирует 99% примеров из rust by examples (т.е. тесты есть)

Имея эту модель, нужно просто писать про неё свои утверждения непосредственно в коке. Т.е. не нужно менять код модели, нужно писать утверждения o модели.

Т.е. например если у нас есть на расте функция (прошу прощения заранее, пример не компилировал, раст больше года не видел)

fn myfun(n) -> nat { return n + 1 }

Lemma myfun_correct n : myfun n = n + 1.

Какая она жуткая…

Ну, я согласен что покрасивее - поприятнее. Но это не очень важно на самом деле. Иногда бывает прям сильно покрасивее получается. Но это вопрос уже конечно некоторых дополнительных усилий - чтобы было красиво.

И в неё достаточно сложно втыкать дополнительные ограничения, которых нет в Rust, так как там нет зависимых типов. А если начинаем что-то втыкать в транслированный код, то автоматически теряем связь с изначальным.

Это не так задумано.
У нас есть исходный код на Расте. Мы транслируем его в код на кок. Это наша модель. С большой долей уверенности можно говорит что она соотвествует оригинальному коду, так как

1) это бекэнд к оригинальному компилятору раста (т.е. парсинг и построение дерева выполняет rustc)

2) транслятор транслирует 99% примеров из rust by examples (т.е. тесты есть)

Имея эту модель, нужно просто писать про неё свои утверждения непосредственно в коке. Т.е. не нужно менять код модели, нужно писать утверждения o модели.

Т.е. например если у нас есть на расте функция (прошу прощения заранее, пример не компилировал, раст больше года не видел)

fn myfn(n) -> nat { return n + 1 }

Lemma myfun_correct n : myfun n = n + 1.

Какая она жуткая…

Ну, я согласен что покрасивее - поприятнее. Но это не очень важно на самом деле. Иногда бывает прям сильно покрасивее получается. Но это вопрос уже конечно некоторых дополнительных усилий - чтобы было красиво.

И в неё достаточно сложно втыкать дополнительные ограничения, которых нет в Rust, так как там нет зависимых типов. А если начинаем что-то втыкать в транслированный код, то автоматически теряем связь с изначальным.

Это не так задумано.
У нас есть исходный код на Расте. Мы транслируем его в код на кок. Это наша модель. С большой долей уверенности можно говорит что она соотвествует оригинальному коду, так как

1) это бекэнд к оригинальному компилятору раста (т.е. парсинг и построение дерева выполняет rustc)

2) транслятор транслирует 99% примеров из rust by examples (т.е. тесты есть)

Имея эту модель, нужно просто писать про неё свои утверждения непосредственно в коке. Т.е. не нужно менять код модели, нужно писать утверждения o модели.

Т.е. например если у нас есть на расте функция (прошу прощения заранее, пример не компилировал, раст больше года не видел)

fn myfn(n) -> nat { return n + 1 }

Lemma myfun_correct n : myfun n = n + 1.

Какая она жуткая…

Ну, я согласен что покрасивее - поприятнее. Но это не очень важно на самом деле. Иногда бывает прям сильно покрасивее получается. Но это вопрос уже конечно некоторых дополнительных усилий - чтобы было красиво.

И в неё достаточно сложно втыкать дополнительные ограничения, которых нет в Rust, так как там нет зависимых типов. А если начинаем что-то втыкать в транслированный код, то автоматически теряем связь с изначальным.

Это не так задумано.
У нас есть исходный код на Расте. Мы транслируем его в код на кок. Это наша модель. С большой долей уверенности можно говорит что она соотвествует оригинальному коду, так как

1) это бекэнд к оригинальному компилятору раста (т.е. парсинг и построение дерева выполняет rustc)

2) транслятор транслирует 99% примеров из rust by examples (т.е. тесты есть)

Имея эту модель, нужно просто писать про неё свои утверждения непосредственно в коке. Т.е. не нужно менять код модели, нужно писать утверждения o модели.

Т.е. например если у нас есть на расте функция

myfun x => x + 1

Lemma myfun_correct n : myfun n = n + 1.

Какая она жуткая…

Ну, я согласен что покрасивее - поприятнее. Но это не очень важно на самом деле. Иногда бывает прям сильно покрасивее получается. Но это вопрос уже конечно некоторых дополнительных усилий - чтобы было красиво.

И в неё достаточно сложно втыкать дополнительные ограничения, которых нет в Rust, так как там нет зависимых типов. А если начинаем что-то втыкать в транслированный код, то автоматически теряем связь с изначальным.

Это не так задумано.
У нас есть исходный код на Расте. Мы транслируем его в код на кок. Это наша модель. С большой долей уверенности можно говорит что она соотвествует оригинальному коду, так как

1) это бекэнд к оригинальному компилятору раста (т.е. парсинг и построение дерева выполняет rustc)

2) транслятор транслирует 99% примеров из rust by examples (т.е. тесты есть)

Имея эту модель, нужно просто писать про неё свои утверждения непосредственно в коке. Т.е. не нужно менять код модели, нужно писать утверждения o модели.

Т.е. например если у нас есть на расте функция

myfun x => x + 1

Lemma myfun_correct n : myfun n = n + 1.