Re: Layout syntax

Hans Aberg wrote:


> <joachim.durchholz@web.de> wrote:
>>After all, proofs aren't just read by computers, they are also read by
>>humans (e.g. to check whether a proof states what was intended, or to
>>modify a proof to prove something slightly different but more
>>interesting), and humans don't parse nested constructs very well.
>
> So it will not be needed to wrote proofs so that
> humans can directly check them, even though humans still must be able
> to write proofs.


I didn't mean checking the validity of the proof - programs for doing
that have been written decades ago.
I meant checking that the theorem being proven is actually what we want
proven. For example, every tax calculation program is an existence proof
for a best way of filling out the tax forms given a set of input
parameters under the constraints of obeying the tax laws. This can also
be done in reverse: when I have a proof that such a solution exists,
without using the law of the excluded middle, then a program that
calculates the value can be automatically derived from the proof.
When I mistype or misinterpret the laws, the program is still a proof
(resp. there's still a specification and an automatically deduced
program), but not for the theorem that I wanted proven.


>>I think we're largely in agreement, and just differ in how far one
>>should go when trying to import mathematical conventions into a
>>computerized language.
>
> Let's generalize typical computer type systems, and see where we might
> land: Hindley-Milner type systems rely on unification to resolve
> polymorphic types. The next generalization might be a type system that
> make use of a Prolog engine, of which unification is a part then. And
> generalizing that, one might instead make use of a proof checking
> engine, based on metamathematics. Then the type system might be
> something like axiomatic set theory. If one gets that far, one has
> unified computer type systems with pure math. :-)


Actually that's a road that I'd like to explore. (I think it's already
being done in academia, though I haven't heard of practial results yet.)


Regards,
Jo

Return to the comp.compilers page.
Search the comp.compilers archives again.