Re: Bitcoin scripting language extensions, collaboration requested
John Nowak <[email protected]> Wed, 05 Feb 2014 17:42:53 -0500
| Newsgroups | gmane.comp.lang.concatenative |
|---|---|
| Message-ID | <[email protected]> |
---QEC-X-tpb10-tma98bc5Cdib0MeyUI9p4b9qfJ
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
On 02/05/2014 04:45 PM, William Tanksley, Jr wrote:
>> First-order applicative languages are easy to give exact resource bounds
>> for if you disallow recursion and dynamic allocation. This has been done
>> quite successfully already (e.g. SPARK Ada).
>
> SPARK Ada should be mentioned, and I hope the Bitcoin people have
> looked at it (Mark?). However, it gains its abilities not by being
> first-order applicative, but rather by having a strong proof language
> tied to a decent and well-known programming language with a
> non-ambiguous subset specification.
The ability to easily calculate resource bounds is precisely due to the
restriction to first-order, recursion-free, allocation-free code: You
can just go through the call tree statically and calculate the maximum
height of the stack. The same thing would be possible even if it offered
no support for proof.
Some of its other abilities I did not mention however, e.g. static array
bounds checking, certainly do require user-provided proofs in some cases.
- jn
---QEC-X-tpb10-tma98bc5Cdib0MeyUI9p4b9qfJ
Content-Type: text/html; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">
<html>
<head>
</head>
<body style="background-color: #fff;">
<span style="display:none"> </span>
<!--~-|**|PrettyHtmlStartT|**|-~-->
<div id="ygrp-mlmsg" style="position:relative;">
<div id="ygrp-msg" style="z-index: 1;">
<!--~-|**|PrettyHtmlEndT|**|-~-->
<div id="ygrp-text" >
<p>On 02/05/2014 04:45 PM, William Tanksley, Jr wrote:<br>
<br>
>> First-order applicative languages are easy to give exact resource bounds<br>
>> for if you disallow recursion and dynamic allocation. This has been done<br>
>> quite successfully already (e.g. SPARK Ada).<br>
><br>
> SPARK Ada should be mentioned, and I hope the Bitcoin people have<br>
> looked at it (Mark?). However, it gains its abilities not by being<br>
> first-order applicative, but rather by having a strong proof language<br>
> tied to a decent and well-known programming language with a<br>
> non-ambiguous subset specification.<br>
<br>
The ability to easily calculate resource bounds is precisely due to the <br>
restriction to first-order, recursion-free, allocation-free code: You <br>
can just go through the call tree statically and calculate the maximum <br>
height of the stack. The same thing would be possible even if it offered <br>
no support for proof.<br>
<br>
Some of its other abilities I did not mention however, e.g. static array <br>
bounds checking, certainly do require user-provided proofs in some cases.<br>
<br>
- jn<br>
</p>
</div>
<!--~-|**|PrettyHtmlStart|**|-~-->
<div style="color: #fff; height: 0;">__._,_.___</div>
<div style="clear:both"> </div>
<table cellspacing=4px style="margin-top: 20px; margin-bottom: 10px;">
<tbody>
<tr>
<td style="font-size: 12px; font-family: arial; font-weight: bold; padding: 7px 5px 5px; color: #FFF; background-color: #F2F2F2; border: 1px solid #EAEAEA " >
<a style="text-decoration: none; color: #2D50FD" href="http://groups.yahoo.com/group/concatenative/post;_ylc=X3oDMTJwaWM5Nm4yBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BG1zZ0lkAzQ5NjUEc2VjA2Z0cgRzbGsDcnBseQRzdGltZQMxMzkxNjQwMTQw?act=reply&messageNum=4965">Reply via web post</a>
</td>
<td style="font-size: 12px; font-family: arial; padding: 7px 5px 5px; color: #FFF; background-color: #F2F2F2; border: 1px solid #EAEAEA; " >
<a href="mailto:[email protected]?subject=Re%3A%20%5Bstack%5D%20Bitcoin%20scripting%20language%20extensions%2C%20collaboration%20requested" style="text-decoration: none; color: #2D50FD;">
Reply to sender </a>
</td>
<td style="font-size: 12px; font-family: arial; padding: 7px 5px 5px; color: #FFF; background-color: #F2F2F2; border: 1px solid #EAEAEA; ">
<a href="mailto:[email protected]?subject=Re%3A%20%5Bstack%5D%20Bitcoin%20scripting%20language%20extensions%2C%20collaboration%20requested" style="text-decoration: none; color: #2D50FD">
Reply to group </a>
</td>
<td style="font-size: 12px; font-family: arial; padding: 7px 5px 5px; color: #FFF; background-color: #F2F2F2; border: 1px solid #EAEAEA; " >
<a href="http://groups.yahoo.com/group/concatenative/post;_ylc=X3oDMTJlMGQyczlpBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwNmdHIEc2xrA250cGMEc3RpbWUDMTM5MTY0MDE0MA--" style="text-decoration: none; color: #2D50FD">Start a New Topic</a>
</td>
<td style="font-size: 12px; font-family: arial; padding: 7px 5px 5px; color: #2D50FD; background-color: #F2F2F2; border: 1px solid #EAEAEA; " >
<a href="http://groups.yahoo.com/group/concatenative/message/4950;_ylc=X3oDMTM0N2Fvc2YyBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BG1zZ0lkAzQ5NjUEc2VjA2Z0cgRzbGsDdnRwYwRzdGltZQMxMzkxNjQwMTQwBHRwY0lkAzQ5NTA-" style="text-decoration: none; color: #2D50FD;">Messages in this topic</a>
(16)
</td>
</tr>
</tbody>
</table>
<!------- Start Nav Bar ------>
<!-- |**|begin egp html banner|**| -->
<div id="ygrp-vital" style="background-color: #f2f2f2; font-family: Verdana; font-size: 10px; margin-bottom: 10px; padding: 10px;">
<span id="vithd" style="font-weight: bold; color: #333; text-transform: uppercase; "><a href="http://groups.yahoo.com/group/concatenative;_ylc=X3oDMTJlbTgzMDFxBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwN2dGwEc2xrA3ZnaHAEc3RpbWUDMTM5MTY0MDE0MA--" style="text-decoration: none;">Visit Your Group</a></span>
<ul style="list-style-type: none; margin: 0; padding: 0; display: inline;">
</ul>
</div>
<div id="ft" style="font-family: Arial; font-size: 11px; margin-top: 5px; padding: 0 2px 0 0; clear: both;">
<a href="http://groups.yahoo.com/;_ylc=X3oDMTJkNGZ2ZzAxBF9TAzk3MzU5NzE0BGdycElkAzE4MzkyNzQEZ3Jwc3BJZAMxNzA1MDA2NzY0BHNlYwNmdHIEc2xrA2dmcARzdGltZQMxMzkxNjQwMTQw" style="float: left;"><img src="http://l.yimg.com/ru/static/images/yg/img/email/new_logo/logo-groups-137x15.png" height="15" width="137" alt="Yahoo! Groups" style="border: 0;"/></a>
<div style="color: #747575; float: right;"> • <a href="http://info.yahoo.com/privacy/us/yahoo/groups/details.html" style="text-decoration: none;">Privacy</a> • <a href="mailto:[email protected]?subject=Unsubscribe" style="text-decoration: none;">Unsubscribe</a> • <a href="http://info.yahoo.com/legal/us/yahoo/utos/terms/" style="text-decoration: none;">Terms of Use</a> </div>
</div>
<!-- |**|end egp html banner|**| -->
</div> <!-- ygrp-msg -->
<!-- Sponsor -->
<!-- |**|begin egp html banner|**| -->
<div id="ygrp-sponsor" style="width:160px; float:right; clear:none; margin:0 0 25px 0; background: #fff;">
<!-- Start Recommendations -->
<div id="ygrp-reco">
</div>
<!-- End Recommendations -->
</div> <!-- |**|end egp html banner|**| -->
<div style="clear:both; color: #FFF; font-size:1px;">.</div>
</div>
<img src="http://geo.yahoo.com/serv?s=97359714/grpId=1839274/grpspId=1705006764/msgId=4965/stime=1391640140" width="1" height="1"> <br>
<div style="color: #fff; height: 0;">__,_._,___</div>
<!--~-|**|PrettyHtmlEnd|**|-~-->
</body>
<!--~-|**|PrettyHtmlStart|**|-~-->
<head>
<style type="text/css">
<!--
#ygrp-mkp {
border: 1px solid #d8d8d8;
font-family: Arial;
margin: 10px 0;
padding: 0 10px;
}
#ygrp-mkp hr {
border: 1px solid #d8d8d8;
}
#ygrp-mkp #hd {
color: #628c2a;
font-size: 85%;
font-weight: 700;
line-height: 122%;
margin: 10px 0;
}
#ygrp-mkp #ads {
margin-bottom: 10px;
}
#ygrp-mkp .ad {
padding: 0 0;
}
#ygrp-mkp .ad p {
margin: 0;
}
#ygrp-mkp .ad a {
color: #0000ff;
text-decoration: none;
}
#ygrp-sponsor #ygrp-lc {
font-family: Arial;
}
#ygrp-sponsor #ygrp-lc #hd {
margin: 10px 0px;
font-weight: 700;
font-size: 78%;
line-height: 122%;
}
#ygrp-sponsor #ygrp-lc .ad {
margin-bottom: 10px;
padding: 0 0;
}
#actions {
font-family: Verdana;
font-size: 11px;
padding: 10px 0;
}
#activity {
background-color: #e0ecee;
float: left;
font-family: Verdana;
font-size: 10px;
padding: 10px;
}
#activity span {
font-weight: 700;
}
#activity span:first-child {
text-transform: uppercase;
}
#activity span a {
color: #5085b6;
text-decoration: none;
}
#activity span span {
color: #ff7900;
}
#activity span .underline {
text-decoration: underline;
}
.attach {
clear: both;
display: table;
font-family: Arial;
font-size: 12px;
padding: 10px 0;
width: 400px;
}
.attach div a {
text-decoration: none;
}
.attach img {
border: none;
padding-right: 5px;
}
.attach label {
display: block;
margin-bottom: 5px;
}
.attach label a {
text-decoration: none;
}
blockquote {
margin: 0 0 0 4px;
}
.bold {
font-family: Arial;
font-size: 13px;
font-weight: 700;
}
.bold a {
text-decoration: none;
}
dd.last p a {
font-family: Verdana;
font-weight: 700;
}
dd.last p span {
margin-right: 10px;
font-family: Verdana;
font-weight: 700;
}
dd.last p span.yshortcuts {
margin-right: 0;
}
div.attach-table div div a {
text-decoration: none;
}
div.attach-table {
width: 400px;
}
div.file-title a, div.file-title a:active, div.file-title a:hover, div.file-title a:visited {
text-decoration: none;
}
div.photo-title a, div.photo-title a:active, div.photo-title a:hover, div.photo-title a:visited {
text-decoration: none;
}
div#ygrp-mlmsg #ygrp-msg p a span.yshortcuts {
font-family: Verdana;
font-size: 10px;
font-weight: normal;
}
.green {
color: #628c2a;
}
.MsoNormal {
margin: 0 0 0 0;
}
o {
font-size: 0;
}
#photos div {
float: left;
width: 72px;
}
#photos div div {
border: 1px solid #666666;
height: 62px;
overflow: hidden;
width: 62px;
}
#photos div label {
color: #666666;
font-size: 10px;
overflow: hidden;
text-align: center;
white-space: nowrap;
width: 64px;
}
#reco-category {
font-size: 77%;
}
#reco-desc {
font-size: 77%;
}
.replbq {
margin: 4px;
}
#ygrp-actbar div a:first-child {
/* border-right: 0px solid #000;*/
margin-right: 2px;
padding-right: 5px;
}
#ygrp-mlmsg {
font-size: 13px;
font-family: Arial, helvetica,clean, sans-serif;
*font-size: small;
*font: x-small;
}
#ygrp-mlmsg table {
font-size: inherit;
font: 100%;
}
#ygrp-mlmsg select, input, textarea {
font: 99% Arial, Helvetica, clean, sans-serif;
}
#ygrp-mlmsg pre, code {
font:115% monospace;
*font-size:100%;
}
#ygrp-mlmsg * {
line-height: 1.22em;
}
#ygrp-mlmsg #logo {
padding-bottom: 10px;
}
#ygrp-msg p a {
font-family: Verdana;
}
#ygrp-msg p#attach-count span {
color: #1E66AE;
font-weight: 700;
}
#ygrp-reco #reco-head {
color: #ff7900;
font-weight: 700;
}
#ygrp-reco {
margin-bottom: 20px;
padding: 0px;
}
#ygrp-sponsor #ov li a {
font-size: 130%;
text-decoration: none;
}
#ygrp-sponsor #ov li {
font-size: 77%;
list-style-type: square;
padding: 6px 0;
}
#ygrp-sponsor #ov ul {
margin: 0;
padding: 0 0 0 8px;
}
#ygrp-text {
font-family: Georgia;
}
#ygrp-text p {
margin: 0 0 1em 0;
}
#ygrp-text tt {
font-size: 120%;
}
#ygrp-vital ul li:last-child {
border-right: none !important;
}
-->
</style>
</head>
<!--~-|**|PrettyHtmlEnd|**|-~-->
</html>
<!-- end group email -->
---QEC-X-tpb10-tma98bc5Cdib0MeyUI9p4b9qfJ--