p
@enomad что тебе конкретно непонятно в доквах?
Size: a a a
2020 October 30
SP
ну чел делает какуюто хуйню и говорит МЫ ДОКАЗАЛИ
b
часто не строится потому что примитивов нет чтобы строить
но в самом общем виде, что дает тебе это чувство уверенности в том, что тот или иной алгоритм или план действий по написанию кода окажется правильным?
SP
тоесть как бы что конкретно он делает? пытается рерайтить выражение чтобы оно было равно другому выражению?
b
в каком–то смысле, можно посмотреть на отдельные запчасти твоей программы и понять, что ее логика опирается на корректность работы тех или иных запчастей
SP
но в самом общем виде, что дает тебе это чувство уверенности в том, что тот или иной алгоритм или план действий по написанию кода окажется правильным?
ну это понятно - ТИПЧИКИ
p
ну чел делает какуюто хуйню и говорит МЫ ДОКАЗАЛИ
Разница между тестом и пруфом:
test: 10 = myfunc 20
proof: (n: Nat) -> (n + 10) = myFunc n
test: 10 = myfunc 20
proof: (n: Nat) -> (n + 10) = myFunc n
p
Понял?
b
то есть можно говорить про твою программу на двух уровнях, как последовательность инструкций организованных в файлы (условную тьюринговую ленту) или про систему логических фактов и утверждений
p
тоесть как бы что конкретно он делает? пытается рерайтить выражение чтобы оно было равно другому выражению?
Да
b
если твоя программа это ПО для супермаркета, то ее логика во многом будет напоминать логику работы супермаркета
b
улавливаешь?
SP
щаща погоди
b
есть такая штука как Curry–Howard correspondence https://ru.wikipedia.org/wiki/Соответствие_Карри_—_Ховарда
p
если твоя программа это ПО для супермаркета, то ее логика во многом будет напоминать логику работы супермаркета
Скорее компании в которой разрабатывали это ПО кек
b
In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relationship between computer programs and mathematical proofs.
b
то есть это принципиальная идея которая позволяет нам вообще что–либо говорить о времени работы какого–либо алгоритма
SP
Разница между тестом и пруфом:
test: 10 = myfunc 20
proof: (n: Nat) -> (n + 10) = myFunc n
test: 10 = myfunc 20
proof: (n: Nat) -> (n + 10) = myFunc n
погоди ты доказал что у этой функции такая сигнатура? или ээм
b
halting problem в общем виде не решается, поэтому нам остается анализ сложности.
SP
(я еще и синтаксис плохо понимаю, да)