История изменений
Исправление AndreyKl, (текущая версия) :
реализовал ты драйвер на залупидрисе, что ты можешь гарантировать в рантайме если тебя вызывает ядро и передаёт тебе указатель на память которую другой драйвер уже освободил, а третий снова выделил её и разместил там свою совсем другую структуру с данными ?
На самом деле вопрос часто задаваемый. Но ответ довольно простой: речь идёт о коде на идрисе, и все гарантии даются на код который написан на идрисе: он проверит весь возможный ввод, не выйдет за пределы массива, сделает то что обещал сделать и завершиться.
Тут главная разница в том, что в отличии от идриса (coq'а, agda'ы), где гарантии даёт компилятор, единственная гарантия которую может дать программист на «более обычном языке» звучит примерно так
Мамой клянусь! Не упадёт. Всё что надо делает!
А так да, ты прав, хоть там хоть там тебе вернёт ядро не ту структуру и будешь сидеть со своими гарантиями. Правда ядро то наверное не твоя зона ответсвенности.. и сколько раз тебе ядро не ту структуру возвращало я даже боюсь спросить.. но это уже детали для практиков, чего «теоретикам» туда лезть, верно? Тут, «в теории», «всё равно».
Исправление AndreyKl, :
реализовал ты драйвер на залупидрисе, что ты можешь гарантировать в рантайме если тебя вызывает ядро и передаёт тебе указатель на память которую другой драйвер уже освободил, а третий снова выделил её и разместил там свою совсем другую структуру с данными ?
На самом деле вопрос часто задаваемый. Но ответ довольно простой: речь идёт о коде на идрисе, и все гарантии даются на код который написан на идрисе: он проверит весь возможный ввод, не выйдет за пределы массива, сделает то что обещал сделать и завершиться.
Тут главная разница в том, что в отличии от идриса (coq'а, agda'ы), где гарантии даёт компилятор, единственная гарантия которую может дать программист на «более обычном языке» звучит примерно так
Мамой клянусь! Не упадёт. Всё что надо делает!
А так да, ты прав, хоть там хоть там тебе вернёт ядро не ту структуру и будешь сидеть со своими гарантиями. Правда ядро то наверное не твоя зона ответсвенности.. и сколько раз интересно тебе ядро не ту структуру возвращало я даже боюсь спросить.. но это уже детали для практиков, чего «теоретикам» туда лезть, верно? Тут, «в теории», «всё равно».
Исправление AndreyKl, :
реализовал ты драйвер на залупидрисе, что ты можешь гарантировать в рантайме если тебя вызывает ядро и передаёт тебе указатель на память которую другой драйвер уже освободил, а третий снова выделил её и разместил там свою совсем другую структуру с данными ?
На самом деле вопрос часто задаваемый. Но ответ довольно простой: речь идёт о коде на идрисе, и все гарантии даются на код который написан на идрисе: он проверит весь возможный ввод, не выйдет за пределы массива, сделает то что обещал сделать и завершиться.
Тут главная разница в том, что в отличии от идриса (coq'а, agda'ы), где гарантии даёт компилятор, единственная гарантия которую может дать программист на «более обычном языке» звучит примерно так
Мамой клянусь! Не упадёт. Всё что надо делает!
А так да, ты прав, хоть там хоть там тебе вернёт ядро не ту структуру и будешь сидеть со своими гарантиями. Правда ядро то наверное не твоя зона ответсвенности.. и сколько раз интересно тебе ядро не ту структуру возвращало я даже боюсь спросить.. но это уже детали для практиков, чего теоретикам туда лезть, верно? Тут, «в теории», «всё равно».
Исходная версия AndreyKl, :
реализовал ты драйвер на залупидрисе, что ты можешь гарантировать в рантайме если тебя вызывает ядро и передаёт тебе указатель на память которую другой драйвер уже освободил, а третий снова выделил её и разместил там свою совсем другую структуру с данными ?
На самом деле вопрос часто задаваемый. Но ответ довольно простой: речь идёт о коде на идрисе, и все гарантии даются на код который написан на идрисе: он проверит весь возможный ввод, не выйдет за пределы массива, сделает то что обещал сделать и завершиться.
Тут главная разница в том, что в отличии от идриса (coq'а, agda'ы), где гарантии даёт компилятор, единственная гарантия которую может дать программист на «более обычном языке» звучит примерно так
Мамой клянусь! Не упадёт. Всё что надо делает!
а так да, ты прав, хоть там хоть там тебе вернёт ядро не ту структуру и будешь сидеть со своими гарантиями. правда ядро то наверное не твоя зона ответсвенности.. но это уже детали для практиков, чего теоретикам туда лезть, верно? Тут, «в теории», «всё равно».