Email Gateway (Aug 23 2022 at 08:28): Email Gateway (Aug 23 2022 at 08:28):From: Talia Ringer <tringer@cs.washington.edu>
Hi all,
I'm curious if any of you have ever started to verify a system, but then
abandoned that system due to the difficulty of evolving and maintaining
your proofs. If so, I would love for you to share those proof efforts with
me, especially if the code is public.
Thanks!
Talia
Email Gateway (Aug 23 2022 at 08:28):From: Talia Ringer <tringer@cs.washington.edu>
To clarify: any size project in any proof assistant is fine. I'd actually
really love examples of projects of different sizes in different proof
assistants. The more examples, the better.
Email Gateway (Aug 23 2022 at 08:28):From: Jose Manuel Rodriguez Caballero <jose.manuel.rodriguez.caballero@ut.ee>
Talia wrote:
I was developing a project of formal verification of my publications concerning a new approach to the number theory that I invented. In XIX century, number theory was approached from the analytic point of view (analytic number theory, e.g., Dirichlet, Riemann), the algebraic point of view (algebraic number theory, e.g., Dedekind, Kronecker), and the geometric point of view (geometry of numbers, Minkowski). My idea was to approach number theory from the point of view of computer science, more specifically, the theory of formal languages (language-theoretic number theory). There were some connections between number theory and formal language before, but it has nothing to do with my approach (this is the reason why I was able to publish my results in good journals, otherwise the editors will reject such a theory).
I was developing a library in Isabelle/HOL and proving some of my theorems. The library is here:
Also, I proved a new result concerning the Erdos-Nicolas function:
Also, here is a theorem that I discovered using my approach:
I stopped this project because I learned from experts of TUM that my implementation in Isabelle/HOL was rather non-constructive, typical a mathematician by training, but it was better to develop a more constructive approach in order to make explicit computations and experiments in Isabelle/HOL. I tried to adapt my library to the approach suggested by the experts. But, because such a project was independent (zero funding), I decided to spend my efforts on some projects with financial support and let the development of language-theoretic number theory for people with less financial need than myself and interested in the subject, if there are any in the future.
Conclusion: the project was abandoned because my skills in Isabelle/HOL, which I learned by myself from the tutorial, were not developed enough at that time and I had no financial motivation in order to update this project when my skills were improved by practice. I think that young mathematicians can develop a creative mathematical research activity in Isabelle/HOL, with the condition of having financial support.
--> Here is the "manifesto" of language-theoretic number theory, which motivated the formal verification of this system:
Caballero, José Manuel Rodrıguez. "Symmetric Dyck Paths and Hooley’s∆-function." Combinatorics on Words. Springer International Publishing AG (2017).
https://www.springerprofessional.de/symmetric-dyck-paths-and-hooley-s-function/14229112
--> Here are some publications of new theorems that I obtained using this approach in the journal INTEGERS:
"Jordan's Expansion of the Reciprocal of Theta Functions and 2-densely Divisible Numbers"
http://math.colgate.edu/~integers/u2/u2.pdf
"Integers Which Cannot Be Partitioned Into an Even Number of Consecutive Parts"
http://math.colgate.edu/~integers/t20/t20.pdf
--> Here a publication in Journal of Number Theory (one of the main journals in this field):
"On a function introduced by Erdos and Nicolas"
https://www.sciencedirect.com/science/article/pii/S0022314X18301999
Kind regards,
José M.
Email Gateway (Aug 23 2022 at 08:29):From: Lawrence Paulson <lp15@cam.ac.uk>
This is unfortunate and rather untypical of attitudes to formalisation in Isabelle/HOL. There are some cases in which interesting executable code can be generated from proofs, but there’s no reason to pretend that Isabelle/HOL is constructive. It absolutely isn’t. Non-constructive proofs are everywhere in the libraries and absolutely welcome.
Larry
Email Gateway (Aug 23 2022 at 08:29):From: Christoph Sprenger <sprenger@inf.ethz.ch>
Dear Talia,
this is not my own proof effort, but I know Diego Ongaro formalized his Raft consensus protocol [1,3] in TLA and partially proved one of its properties in the TLA prover. He later abandoned the effort to prove further properties, since he “found it too tedious and time-consuming to use the TLA proof system at the scale of a complete proof” [2, Section 8.2], see also [1, Section 8.2].
Cheers,
Christoph
—
[1] https://www.usenix.org/conference/atc14/technical-sessions/presentation/ongaro <https://www.usenix.org/conference/atc14/technical-sessions/presentation/ongaro>
[2] https://web.stanford.edu/~ouster/cgi-bin/papers/OngaroPhD.pdf <https://web.stanford.edu/~ouster/cgi-bin/papers/OngaroPhD.pdf>
[3] https://raft.github.io/ <https://raft.github.io/>
Email Gateway (Aug 23 2022 at 08:29):From: Denis Nikiforov <denis.nikif@gmail.com>
Hi
I formalized the semantics of the OCL language:
https://www.isa-afp.org/entries/Safe_OCL.html
Here is a significantly improved version of the theory:
https://github.com/AresEkb/Safe_OCL
I added new data types, added a concrete syntax, refactored the type system
and changed semantics of some operations after discussion with a main OCL
contributor.
The project has two goals:
1) Provide a simple reference formalization of a real (non-toy) language
for people far from mathematics (for engineers like me). There are a lot of
examples of toy languages, but when you start to formalize a more
complicated language it's not an easy task. Formalizations of other
languages (Java, etc.) are too complicated for me.
2) Improve OCL language itself.
However, I don't have time to finish it. I hope I'll do it in future.
вс, 16 февр. 2020 г. в 06:28, Talia Ringer <tringer@cs.washington.edu>:
Email Gateway (Aug 23 2022 at 08:29):From: Jose Manuel Rodriguez Caballero <jose.manuel.rodriguez.caballero@ut.ee>
For a mathematician who is working in a new subject, e.g., a new theorem in combinatorics, Isabelle/HOL can be used as a personal notebook, in order to keep track of the consistency and the progress in the proofs. Nevertheless, after obtaining his/her desired proof, the mathematician will write a paper about that subject and he/she will jump to the next subject. So, the notebook library may be abandoned, because the mathematician is measured in academia by his/her publications on journals about mathematics. The draft in Isabelle/HOL, as any draft, will not be optimal.
A possible solution in order to make the notebook library a file good enough for publication in Archives of Formal Proofs is to develop a software in order to automatically improve the code written by the mathematician as a draft. This automatic improvement may even help the mathematician to write his/her paper for the journal of mathematics.
Kind regards,
José M.
Email Gateway (Aug 23 2022 at 08:29):From: "Fernandez, Matthew" <matthew.fernandez@intel.com>
Some of the Elasticsearch algorithms have been verified using TLA+ [0]. In that repository is also a partial Isabelle formalization of the same. I had a conversation with David Turner about why they moved away from Isabelle to TLA+, but can't recall the exact details and motivation offhand. This might be an interesting case study for you though, Talia.
[0]: https://github.com/elastic/elasticsearch-formal-models
Email Gateway (Aug 23 2022 at 08:29):From: Stephan Merz <stephan.merz@loria.fr>
A short look at the GitHub repository seems to indicate that they moved to model checking. Although an interactive proof system for TLA+ does exist, I couldn't see any proofs in their modules.
Stephan
Email Gateway (Aug 23 2022 at 08:29):From: "Fernandez, Matthew" <matthew.fernandez@intel.com>
Yes, I was not meaning to imply otherwise. Merely that I don't recall the reason why they moved away from ITP. You can see the Isabelle pieces under cluster/isabelle in the repository.
Last updated: Nov 21 2024 at 12:39 UTC