Can the language of proof assistants be used for general purpose programming?
proofassistants.stackexchange.com
proofassistants.stackexchange.com
You can use it for general purpose programming, but it's very difficult and various degrees of verification you can achieve with it [3]. I made a verified version of Rob Pike's simple C regex matcher in SPARK -- proving an absence of runtime errors (e.g. never raise an exception or hit an out of bounds condition).
[1]: https://alire.ada.dev/crates.html
[2]: https://github.com/rod-chapman/SPARKNaCl
[3]: https://blog.adacore.com/from-ada-to-platinum-spark-a-case-s...
That is also VHDL, which is based on Ada, is also mostly used in Europe in detriment to Verilog.
FOSDEM tends to have a regular Ada room.
Besides military, there is avionics, transport, critical factory infrastructure, lots of stuff that falls under high integrity computing.
Alas FOSDEM has changed its room attribution scheme for 'smaller' communities and IIUC there was no Ada room this year. Hopefully there'll be a space next year.
https://blog.adacore.com/nvidia-security-team-what-if-we-jus...
At the same time of this update of the language, a large effort was in progress to modernise the 'old' spark that used contacts and proof annotations in Ada code through some kind of comment-based language.
The 'merge' here was to make contracts and proof annotations actually executable Ada code (when it made sense).
SPARK is first a toolsuite that examines Ada code to prove properties on this code (variable initialisation, dataflow properties, absence of runtime retors, partial or complete functional specification). The proverbe tech being only so capable, they had to restrict the supporterd language features (calling it the 'SPARK subset') for a while (most of the restrictions have been lifted in the recent year such as dynamic allocation, exceptions, aliasing) and some very hard things improved too (e.g. floating point handling).
Also, to be complete, since executable contracts are not always enough, they introduced in the Ada language (for SPARK) what they call ghost code (seen and used only by the proof tools).
So, yes, in a way SPARK features were merged in Ada, but you won't be able to use them for proof without the proof tools, you'll have a very expressive form of runtime assertion. Some features actually cascaded back to the compiler and the actual Ada language implementations.
Also, to be easier to use for proof, the Ada2012 and 2022 language specs added a lot of sugar: quantifiers, if-expressions, case-expressions, raise-expressions, but also delta-aggregates... all greatly improving the expressivity of Ada.
I've loved being able to use Lean's macro system to write JSX-like HTML:
def header := <header class_="header">
<h1>todo</h1>
...
I would love to be able to write types that describe, e.g., assumptions made about external resources, so that I can prove that "assuming my DB has such-and-such a latency, my page will always render in such-and-such a time" or something similar - but it's a bit beyond me at the moment.
[1] https://github.com/alex-wellbelove/LeanServer [2] https://hackage.haskell.org/package/servant
Change the need to be really good at proglog to just need to distinctly describe what want/need.
Whether AI produces Lean code or a human produces Lean code... The Lean code should speak for itself. Both humans and AI are the weak link in either case, and it's unclear to me which of the two is the weaker.
If it manages to produce successful proofs of pre-existing property specifications, then that's great!
My thinking is still pretty fuzzy. But I feel like there's something important and valuable with the idea of "this is the specification of the software" and the "this software meets that specification".
Now, yes, maybe the specification is wrong. Proofs are hard to write. All software has a bunch of implicit constraints. I forget them for the code I wrote, and it's even tougher to figure them out when I'm handed a legacy project where the author is long gone.
There's something really important about that dual view of, this is what it's supposed to do, and this is what it does. And tools can help check that they agree!
There's like the classic Haskell example of verified email - at some point the user was sent an email and they clicked a link, so that string is special, pretty sure foo@example.com is a real email.
The ability to slap a type on something, then have tools tell you "this is everything that needs to be updated" is really appealing. Like, The account must be in good standing before shipping product. So I keep puttering around with it.
It's often difficult to add features and be super sure you're not breaking stuff. Well, maybe not you, but me, for sure.
Isn’t this the whole concept behind writing tests?
But there are some things that are challenging to test for. Tests sample the space, proofs define the space. you can't build it wrong. (you can sure have a bad spec, and build the wrong thing though)
Tests definitely help. It sorta feels like there's value left on the table. The spec, the types let you define broader constraints, and you catch them all.
- Start with spec. - Write the specs as something that the compiler/test harness will check for you. - Write the code.
The main differences being, of course, that you'll typically get your compiler error messages much faster than your test error messages (typically while you're writing the code), which makes them easier to fix - on the other hand, in pretty much all languages, the type system isn't expressive enough to represent all the specs that can be represented as tests.
In other words, in the current state of the world, we need both.
I view the type system as a way to whittle down the state space to the bare minimum while the tests validate that that the behavior of that whittled down execution space matches what is required.
I think investment in a type system to replace tests very quickly reaches a point of diminishing returns and vice versa. A really good type system won't ever beat ok tests + an ok type system and vice versa.
Also, I have seen people write proofs in Coq and extract them to compilable OCaml source code.
I wonder if LLMs could help here? It's a burden to write the proofs, but if LLMs become good enough and flexible enough, the dependant type system might serve as a formal layer on top of a LLM, while the LLM fills in the proofs for us.
A dependant type system could serve as the "world" an AI lives and grows in. Currently LLMs mimic our words without a reality to push back. LLMs can't be wrong, they try to mimic, but they have no hard limitations, whatever word they spit out has only soft rewards or punishments. A type system could be the reality an AI lives and learns in, with a hard ground it can fall on, hard walls it cannot pass, and other hard limitations it can explore in.
[1] https://ericpony.github.io/z3py-tutorial/guide-examples.htm
You can write proofs in a non-interactive way, but you're signing yourself up for a lot of tedium.
EDIT: A video showing someone working through some simple stuff. You can obviously do a lot of things "in your head" but having the feedback loop is helpful. Though thinking about it more I don't think this precludes a Python DSL entirely. It would just require some smart design to support this form of interactivity. https://www.youtube.com/watch?v=VYFTph2izIs
Or do you mean a Python-like syntax on top of Lean4?
Note: Pretty sure that libtorch is written in C++ and CUDA.
Theorem provering languages are cool. Being able to prove the absence of bugs, enforce complex invariants, etc. is cool and useful in certain cases (like cryptography and safety-critical software). But it's also very hard, at least state-of-the-art, so often I feel writing good tests is better.
L4 is less a simplified kernel and more of a microkernel, but it is fully general purpose.
One of the neat things they did was transport memory/resource management to userland and maintain a strict capabilities scheme for ensuring correctness. The other was the cost estimate they claim, which was something like a 60% cost saving for doing the formally verified programming compared to standard ‘high assurance’ programming.
It was a cool project but is not often used to support further pushes into more general systems level applicability of ‘theorem proving’ based programming languages.
Working on a number of platforms, verified on some. Multicore support is an ongoing effort afaict.
An OS built on this kernel is still subject to some assumptions (like, hardware working correctly, bootloader doing its job, etc). But mostly those assumptions are less of a problem / easier to prove than the properties of a complex software system.
As I understand it, guarantees that seL4 does provide, go well beyond anything else currently out there.
However, both CompCert and sel4 took a few years to develop, whereas it would only take months if not weeks to make versions of both which aren't formally verified but heavily tested.