On rebooting: the unreasonable effectiveness of turning computers off and on

Re:On rebooting: the unreasonable effectiveness of turning c... by librexpr on Wednesday May 25, 2022 @04:23AM (#31501872)

I just want to point out that you don't need to know the precise bounds of such a computational model to prove things about your programs. There already exist Turing-complete programming languages where you can prove non-trivial properties about your program and which have had practical applications, for example F* and its use in Project Everest.

https://project-everest.github.io/

https://www.fstar-lang.org/

[ Parent | on HN ]

Re:On rebooting: the unreasonable effectiveness of turning c... by mkleczek on Wednesday May 25, 2022 @05:31AM (#31502239)

Just having a language that allows you to prove things does not mean it is possible to prove them.

We still don't know if it is possible to build a provably correct multi-tasking OS or a web browser without security vulnerabilities. If it was easy we would already have one written in FStar or Idris.

While admiring all the work done by Project Everest - the fact is that it is a multi-year project (I first read about it about 3-4 years ago and it was already under way) with a very limited scope - it is more of an evidence of difficulties of writing correct software.

[ Parent | on HN ]