[M3devel] Legacy of Modula-3

[Daniel Alejandro Benavides D.]

Hello folks:I admire you too much because keep my learning and what a surprise, the underlying theory of JVM verifier in its latest version, (in the sense of bytecode verifier, not JVM architecture exerciser which AFAIK is proprietary, but heck we have VAX one) is derived from Cardelli/Nelson veneer (with Cardelli-Abadi seminal work on Baby Modula-3 and a Theory of objects as Nelson/George Necula Peter Lee Proof Carrying code).As I understand these type systems are so solid and strong that you can prove besides programs don't go wrong many more properties than simpler systems can, e.g security. See [1]:https://docs.oracle.com/javase/specs/jvms/se7/html/jvms-0-preface7.html
Keep the language alive folks

 
[1] «CiteSeerX — Towards Secure Bytecode Verification on a Java Card». [On line]. Available on: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.4920. [Accesed: 13-oct-2017].


 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://m3lists.elegosoft.com/pipermail/m3devel/attachments/20171013/20ed817a/attachment.html>