51–60 of 64 posts
I believe future of programming would vaguely be some mix of intelligent code generation (e.g. LLMs) + formal verification. "LLMs" would be the compiler of the future, something like gcc today, converting "human" language into machine code.
I wonder why AI doesn't do this verification already. It's a sufficiently simple routine task that doesn't require great precision.
This is great and could provide additional guardrails on top of large language models. I imagine we could provide a more rigorous approach to prove that a LLM can behave in certain ways within a workflow.
In what situations would one prefer this vs Lean? This seems to compile to native code if desired, so does that mean it’s faster than Lean? Forgive me if these are obvious questions, I’m just curious and on my phone right now away from my machine.
Lean has very little support for proving things about software. Right now, the community is mainly geared towards mathematics. This could change. Concrete Semantics was rewritten in Lean [1], but I haven't seen more efforts geared towards software in the Lean community. Dafny, Isabelle, Why3, Coq and F* have been used to verify non-trivial software artifacts. Liquid Haskell, Agda and others are also interesting, but…
For example their formal specification of their ledger system:
https://drops.dagstuhl.de/storage/01oasics/oasics-vol118-fmb...
This is great and could provide additional guardrails on top of large language models. I imagine we could provide a more rigorous approach to prove that a LLM can behave in certain ways within a workflow.
Examples of both:
https://sumitkumarjha.com/papers/2023_ICAA_LLM_Dehallucinati...
Even C# suffers from that, though it is a nice language.
For a programming language to have success it needs to be
* opensource * well maintained * first class citizen on win/lin/mac
Never used it, but https://github.com/project-everest/mitls-fstar always seems an incredibly cool thing. Huh, apparently there's a successor to F* called F7 ( https://github.com/mitls/mitls-flex ) ?
Looks like it's a predecessor https://www.microsoft.com/en-us/research/project/f7-refineme...
Earlier quoted context omitted.
Do you think you might be able to elaborate a little bit more about this? I was skimming the "Proof-Oriented Programming" book, and it seems that the primary way to execute F* programs is by extraction or trusted compilation (same as Rocq and Lean, for example). Does F* have some special way to work directly with realistic source code that these other systems don't?
F* is a programming language with proof support. Lean/Coq are theorem providers that can be used to model and generate code. In Coq, there's not a standard way to generate code, you might model and create code many different ways. F* seems to bring this in as the central goal of the language. So I'm discussing this structural difference. F* has an SMT solver, but Lean can import an SMT solver. So the goal is the impo…
Lean is also a programming language with proof support. It is very much in the same category as F* in this regard, and not in the same category as Coq (Rocq).
Earlier quoted context omitted.
F* is a programming language with proof support. Lean/Coq are theorem providers that can be used to model and generate code. In Coq, there's not a standard way to generate code, you might model and create code many different ways. F* seems to bring this in as the central goal of the language. So I'm discussing this structural difference. F* has an SMT solver, but Lean can import an SMT solver. So the goal is the impo…
> F* is a programming language with proof support. Lean/Coq are theorem providers that can be used to model and generate code. Lean is also a programming language with proof support. It is very much in the same category as F* in this regard, and not in the same category as Coq (Rocq).
I believe future of programming would vaguely be some mix of intelligent code generation (e.g. LLMs) + formal verification. "LLMs" would be the compiler of the future, something like gcc today, converting "human" language into machine code.
I wonder if the proliferation of programming languages we saw in the last decade is due to the fact that nowadays it's extremely easy to create one or that existing ones sucks?
It did happen over early things like IRC and the like, but the audience was limited, and the data was ephemeral.
For example, Byte Magazine has an article on writing your own assembler in 1977 [0]: "By doing it yourself you can learn a lot about programming and software design as well as the specs of your own microcomputer, save yourself the cost of program development, and produce a customized language suited to your own needs or fancies."
Programmers have been creating their own languages since the beginning. It's part of why we lean so heavily towards standards - so other people don't break the things we've already built.
[0] https://archive.org/details/best_of_byte_volume_1_1977_06