thanks.
(i now go waxing pointlessly philosophic…) it might be any of:
(a) there is no single high mechanism. decomposition with functional
type constructors vs. object oriented approaches are in some sense a
"dual" of each other (oo is good when the operations are known and
fixed, and you add new types, etc. etc.)
(b) we can find a good high mechanism from things we already know.
some way of advancing a paradigm we do know, or of mixing paradigms.
© the high mechanism required radically new thought cf. rdp or
something (http://awelonblue.wordpress.com/)
we’ll probably only know 10 years after it has been invented and used
enough for us to see that it is the right way to go?
i’m glad you are trying new ideas in this realm. obviously if nobody
is trying new ideas, we’ll never find the high mechanism.
hi Jonathan,
cool! have you advertised this anywhere else?? seems like something
worth posting on e.g. www.lambda-the-ultimate.org and y combinator,
and the ocaml list; those kinds of things 
ok i do see it on the
coq list and stuff, cool. i think it would be great to put up on LtU.On Mon, Jul 14, 2014 at 12:57 PM, Jonathan joni...@gmail.com wrote:
On 07/14/2014 02:52 PM, gmhwxi wrote:
I really don’t have a precise definition for “high-mechanism”.
This is a paragraph I wrote a while ago:
(* ****** ****** *)
I do
not know how to precisely define what a high-mechanism is. Roughly
speaking, it is some kind of feature that allows the programmer to
quickly
produce code that would otherwise take much more time and effort to
write.My own attempt at a “high-mechanism” :
GitHub - jonleivent/mindless-coding: Mindless, verified (erasably) coding using dependent types– Jonathan
–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/53C43621.5080500%40gmail.com.
I really don’t have a precise definition for “high-mechanism”.
This is a paragraph I wrote a while ago:
(* ****** ****** *)
I do
not know how to precisely define what a high-mechanism is. Roughly
speaking, it is some kind of feature that allows the programmer to quickly
produce code that would otherwise take much more time and effort to write.
My own attempt at a “high-mechanism” :
– Jonathan
At this point, it is probably fair to say that F* does not yet have a
“high-mechanism”
to support general-purpose programming.
i apologize for being slow – what do you mean by the high-mechanism?
is there something in ATS(/2) or is it still an open research topic?
thank you.
I did not use it but I did read some of the presented code written in F*.
At this point, it is probably fair to say that F* does not yet have a
“high-mechanism”
to support general-purpose programming.
I have been talking about program-first program verification for some time.
For general
purpose programming, program verification only makes sense if one can have
an effective
way to produce programs to be verified in the first place.On Friday, July 11, 2014 5:28:58 PM UTC-4, Raoul Duke wrote:
You are welcome to post it wherever you feel it would be well received!
You are welcome to post it wherever you feel it would be well received!
'Mindless coding': following proof steps makes algorithms easy | Lambda the Ultimate
martin
wow, and somebody already posted it here a month back, i probably
filed it away w/out having the time then to go actually read up on it.
sheesh. so i’m glad you repeated it :-)On Mon, Jul 14, 2014 at 1:48 PM, Raoul Duke rao...@gmail.com wrote:
hi Jonathan,
cool! have you advertised this anywhere else?? seems like something
worth posting on e.g. www.lambda-the-ultimate.org and y combinator,
and the ocaml list; those kinds of things
coq list and stuff, cool. i think it would be great to put up on LtU.On Mon, Jul 14, 2014 at 12:57 PM, Jonathan joni...@gmail.com wrote:
On 07/14/2014 02:52 PM, gmhwxi wrote:
I really don’t have a precise definition for “high-mechanism”.
This is a paragraph I wrote a while ago:
(* ****** ****** *)
I do
not know how to precisely define what a high-mechanism is. Roughly
speaking, it is some kind of feature that allows the programmer to
quickly
produce code that would otherwise take much more time and effort to
write.My own attempt at a “high-mechanism” :
GitHub - jonleivent/mindless-coding: Mindless, verified (erasably) coding using dependent types– Jonathan
–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/53C43621.5080500%40gmail.com.
hi Jonathan,
cool! have you advertised this anywhere else?? seems like something
worth posting on e.g. www.lambda-the-ultimate.org and y combinator,
and the ocaml list; those kinds of things
coq list and stuff, cool. i think it would be great to put up on LtU.
So far, I have only mentioned it on the Coq list and (briefly) OCaml
list, although a few Idris developers know about it as well.
You are welcome to post it wherever you feel it would be well received!
– Jonathan
Mindless, Verified (Erasably) Coding using Dependent Types | Lobsters
the comment there reflects my wish that i had the time & somebody had
the willingness to teach me how to use Coq & Ocaml & ‘Mindless’
programming some day
I really don’t have a precise definition for “high-mechanism”.
This is a paragraph I wrote a while ago:
(* ****** ****** *)