4 ms·
I would love to see an example of a proof for something like a text editor. How can people be expected to do this when the examples are always trivial toys, li
by taybin 2mo ago
I would love to see an example of a proof for something like a text editor. How can people be expected to do this when the examples are always trivial toys, like array sorting? Show me a formal proof of something that in the trenches programmers can copy from. A proof of a basic todo list or something like that.
- bluGill 2mo agoThat is always my problem too. I can see how to prove sort, if I was writing the standard library for my language I might do that (it is hard, but I hope whoever wrote my library did). However sort is already in my library. I'm writing code that does things much harder to write into a spec.
- warkdarrior 2mo agoMy guess is that the formal spec for a basic TODO list app is the same size as the source code of the app itself.
- antonvs 2mo agoI would not be even slightly surprised if it were larger.
- mrkeen 2mo ago> A proof of a basic todo list or something like that. Just using a verb here would be a first step toward rigorous thinking. A proof that a todo list does what?
- nickpsecurity 2mo agoI believe I proposed that somewhere because it was a small, useful app which often opened malicious payloads. People may or may not fully prove it. What I thought would be useful is, like Ironsides DNS, a SPARK Ada or other implementation that shows no code injections could ever happen from loading, modifying, or rendering text. That's a useful subset of full verification. If not that verified, writing things in a memory-safe, concurrecy-safe language covers lots of ground. Rust and Pony put good effort in those areas. In Rust, I think you still had to manually turn on checks for some overflows which hurt performance a lot. So, static analyzers or automated provers for range properties have a performance benefit. Muen is the largest, production project I know in such a language: https://muen.sk/ https://muen.sk/ Ironsides was an earlier project: https://ironsides.martincarlisle.com/ https://ironsides.martincarlisle.com/